diff options
| author | Jed Barber <jjbarber@y7mail.com> | 2016-12-15 14:28:31 +1100 |
|---|---|---|
| committer | Jed Barber <jjbarber@y7mail.com> | 2016-12-15 14:28:31 +1100 |
| commit | 5395287cc2f758d94bec8befe8956ba2dcc3940c (patch) | |
| tree | fca41713cd7f8a27d41ba0d186adc1e616cf447b /readme.txt | |
| parent | 2fc745bef05860e16a2e89e465a30dc59b5ec2e5 (diff) | |
Old uncommitted changes
Diffstat (limited to 'readme.txt')
| -rw-r--r-- | readme.txt | 102 |
1 files changed, 51 insertions, 51 deletions
@@ -1,51 +1,51 @@ - - -Semantic <input file> - -Evaluates a proof trace, and shows the contents of the Dictionary, Assumptions, Stack and Theorems when done. - - - - -Syntactic <input file> - -Checks a proof trace for syntax errors. - - - - -ProofGraph <input file> - -Constructs a DAG dependency graph of the virtual machine commands used in a given proof trace. - - - - -WriteProof <input file> > <output file> - -Reads a proof trace in, converts it to a DAG a la ProofGraph, then converts it back into a linear proof trace. - - - - -Delete <input file> [<num#1>, <num#2>, <num3>] > <output file> - -Removes all theorems of specified numbers from a proof trace. Best used in conjunction with ListThm, so you can -actually know what theorems are what. Generates a simplified proof trace as output. - - - - -Concat <input #1> <input#2> <input #2> > <output file> - -Joins two proof traces together, converts it to a DAG and back again, then outputs the result. - - - - -ListThm <input file> - -Displays numbered theorems from a proof trace. Best used in conjunction with Delete so you know what theorems you -are deleting. - - +
+
+Semantic <input file>
+
+Evaluates a proof trace, and shows the contents of the Dictionary, Assumptions, Stack and Theorems when done.
+
+
+
+
+Syntactic <input file>
+
+Checks a proof trace for syntax errors.
+
+
+
+
+ProofGraph <input file>
+
+Constructs a DAG dependency graph of the virtual machine commands used in a given proof trace.
+
+
+
+
+WriteProof <input file> > <output file>
+
+Reads a proof trace in, converts it to a DAG a la ProofGraph, then converts it back into a linear proof trace.
+
+
+
+
+Delete <input file> [<num#1>, <num#2>, <num3>] > <output file>
+
+Removes all theorems of specified numbers from a proof trace. Best used in conjunction with ListThm, so you can
+actually know what theorems are what. Generates a simplified proof trace as output.
+
+
+
+
+Concat <input #1> <input#2> <input #2> > <output file>
+
+Joins two proof traces together, converts it to a DAG and back again, then outputs the result.
+
+
+
+
+ListThm <input file>
+
+Displays numbered theorems from a proof trace. Best used in conjunction with Delete so you know what theorems you
+are deleting.
+
+
|