Experimental hol-light version, not usable yet

1 files changed, 32 insertions, 0 deletions

diff --git a/hol-light/example.ml b/hol-light/example.ml
new file mode 100644
index 00000000..ccd59c23
--- /dev/null
+++ b/hol-light/example.ml
@@ -0,0 +1,32 @@
+(*
+    Example proof script for HOL Proof General.
+
+    $Id$
+*)    
+
+g `A /\ B ==> B /\ A`;;
+e DISCH_TAC;;
+e CONJ_TAC;;
+e (IMP_RES_TAC AND_INTRO_THM);;
+e (IMP_RES_TAC AND_INTRO_THM);;
+
+goal `A && B ==> B && A`;
+val and_comms = pg_top_thm_and_drop();;
+
+(* Hints about HOL Proof General:
+ 
+   Proof General needs to work with top-level declarations throughout,
+   and with "interactive" rather than "batch" versions of proofs.
+
+   For best results, theorems should be saved in the way that they are
+   saved above, with pg_top_thm_and_drop.  The function isn't
+   mysterious, it is defined as:
+
+    fun pg_top_thm_and_drop () = let val t = top_thm(); in (drop(); t) end;
+*)
+
+(* this simple proof is not quite like proofs in the other systems,
+   can anyone tell me a more similar proof in HOL? I want to split 
+   the IMP_RES_TAC into two steps.  
+*)
+