From c64deab10f68f15b62ce36adf2970825c7b091de Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 23 Mar 2000 16:36:09 +0000 Subject: Hooray, I proved a theorem. --- hol98/example.sml | 18 +++++------------- 1 file changed, 5 insertions(+), 13 deletions(-) (limited to 'hol98') 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 -- cgit v1.2.3