diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-23 16:36:09 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-23 16:36:09 +0000 |
| commit | c64deab10f68f15b62ce36adf2970825c7b091de (patch) | |
| tree | 334b1b7e3cc51b446d2eca717f3d08bdac83589b /hol98 | |
| parent | b74d7ff99cefe5ef2606fd6fb699c41882e01415 (diff) | |
Hooray, I proved a theorem.
Diffstat (limited to 'hol98')
| -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 |