summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJed Barber <jjbarber@y7mail.com>2012-08-09 05:24:08 +1000
committerJed Barber <jjbarber@y7mail.com>2012-08-09 05:24:08 +1000
commit4797fad4d7da8d667239b5b5049edb5929d09d8b (patch)
tree18f13ac0b48389dfeb598ded094cb1b5156e3995
parent71dce766656c2ae0a6db5cb4befa35cd9dd2f661 (diff)
Concat explanation added
-rw-r--r--README8
1 files changed, 5 insertions, 3 deletions
diff --git a/README b/README
index cd9747d..9a55603 100644
--- a/README
+++ b/README
@@ -28,15 +28,17 @@ Reads a proof trace in, converts it to a DAG a la ProofGraph, then converts it b
-Delete <input file> [<num#1>, <num#2>, <num3>]
+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.
+actually know what theorems are what. Generates a simplified proof trace as output.
-Concat <input #1> <input#2>
+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.