summaryrefslogtreecommitdiff
path: root/README
diff options
context:
space:
mode:
authorJed Barber <jjbarber@y7mail.com>2014-04-08 15:06:40 +1000
committerJed Barber <jjbarber@y7mail.com>2014-04-08 15:06:40 +1000
commit03d38eb3190eb5e51fb18847fe0792013285bde5 (patch)
tree1060d26d3042b5c0c5b1c027fac45fe87f3d685a /README
parentf2c4e4614613ede497f19ef79dc7dc157eaca834 (diff)
Reorganising source code
Diffstat (limited to 'README')
-rw-r--r--README51
1 files changed, 0 insertions, 51 deletions
diff --git a/README b/README
deleted file mode 100644
index 9a55603..0000000
--- a/README
+++ /dev/null
@@ -1,51 +0,0 @@
-
-
-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.
-
-