This editor is very much still under construction. To see an example of a SCRML file, click . That example has the fundamental components of claims and logic, and even a simple proof at the bottom. The proof is that doubly negating true yields true, or Not(Not(True))=True, but in SCRML form.