diff options
Diffstat (limited to 'hol-light/example.ml')
| -rw-r--r-- | hol-light/example.ml | 32 |
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. +*) + |