diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-09 11:03:17 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-09 11:03:17 +0000 |
| commit | a1f38c7d643246761804359354c11c6c183a9d20 (patch) | |
| tree | b19e06a81212877e6a256e5fc53cc643a455d335 /hol98/example.sml | |
| parent | ef92ca36c2390a7779766ab0fa65bbee6ca5d9f9 (diff) | |
First bash at HOL support, working but barely
Diffstat (limited to 'hol98/example.sml')
| -rw-r--r-- | hol98/example.sml | 22 |
1 files changed, 22 insertions, 0 deletions
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. *) + + + + + + + + + |