diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-24 20:16:32 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-24 20:16:32 +0000 |
| commit | 23b798c81fc9c496e6e86108c0fca3715c7f1def (patch) | |
| tree | 498470d06bac6b1d9b1789b454af6149e63eb225 /hol98 | |
| parent | 30d3dd71fe485f9b7a38c1133ec9d2e36a505d46 (diff) | |
Use pg command pg_top_thm_and_drop
Diffstat (limited to 'hol98')
| -rw-r--r-- | hol98/example.sml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/hol98/example.sml b/hol98/example.sml index c0f90e1a..bdc3680e 100644 --- a/hol98/example.sml +++ b/hol98/example.sml @@ -9,7 +9,8 @@ e DISCH_TAC; e CONJ_TAC; e (IMP_RES_TAC AND_INTRO_THM); e (IMP_RES_TAC AND_INTRO_THM); -val and_comms = top_thm(); drop(); +val and_comms = pg_top_thm_and_drop(); + (* this is not quite like proofs in the other systems, can anyone tell me a more similar proof in HOL? |