From 71dce766656c2ae0a6db5cb4befa35cd9dd2f661 Mon Sep 17 00:00:00 2001
From: Jed Barber <jjbarber@y7mail.com>
Date: Thu, 9 Aug 2012 05:21:39 +1000
Subject: Instructions on how to use the programs

---
 README | 49 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)

diff --git a/README b/README
index e69de29..cd9747d 100644
--- a/README
+++ b/README
@@ -0,0 +1,49 @@
+
+
+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>]
+
+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.
+
+
+
+
+Concat <input #1> <input#2>
+
+
+
+
+ListThm <input file>
+
+Displays numbered theorems from a proof trace. Best used in conjunction with Delete so you know what theorems you
+are deleting.
+
+
-- 
cgit