diff options
Diffstat (limited to 'hol98/example.sml')
-rw-r--r-- | hol98/example.sml | 18 |
1 files changed, 5 insertions, 13 deletions
diff --git a/hol98/example.sml b/hol98/example.sml index 64858140..873f0f5f 100644 --- a/hol98/example.sml +++ b/hol98/example.sml @@ -7,17 +7,9 @@ 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. *) - - - - - - - - +e (IMP_RES_TAC AND_INTRO_THM); +e (IMP_RES_TAC AND_INTRO_THM); +val and_comms = top_thm(); drop(); +(* this is not quite like the other proofs, + can anyone tell me a more similar proof in HOL? *)
\ No newline at end of file |