diff options
-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? |