From a1f38c7d643246761804359354c11c6c183a9d20 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Thu, 9 Mar 2000 11:03:17 +0000
Subject: First bash at HOL support, working but barely

---
 hol98/example.sml | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 hol98/example.sml

(limited to 'hol98/example.sml')

diff --git a/hol98/example.sml b/hol98/example.sml
new file mode 100644
index 00000000..04b3b062
--- /dev/null
+++ b/hol98/example.sml
@@ -0,0 +1,22 @@
+(*
+    Example proof script for HOL Proof General.
+
+    $Id$
+*)    
+
+g `A /\ B ==> B /\ A`;
+e DISCH_TAC;
+e CONJ_TAC;
+
+
+(* Ooops, I'm stuck now.  Can somebody help?? 
+   Just want a simple low-level proof here. *)
+
+
+
+
+
+
+
+
+
-- 
cgit v1.2.3