From 23b798c81fc9c496e6e86108c0fca3715c7f1def Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 24 Mar 2000 20:16:32 +0000 Subject: Use pg command pg_top_thm_and_drop --- hol98/example.sml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'hol98') 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? -- cgit v1.2.3