From 1f47fa17959174e05904eae19abd4c23930d56ff Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 23 Mar 2000 18:04:40 +0000 Subject: Comment --- hol98/example.sml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/hol98/example.sml b/hol98/example.sml index 873f0f5f..c0f90e1a 100644 --- a/hol98/example.sml +++ b/hol98/example.sml @@ -11,5 +11,6 @@ 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 +(* this is not quite like proofs in the other systems, + can anyone tell me a more similar proof in HOL? + I want to split the IMP_RES_TAC into two steps. *) \ No newline at end of file -- cgit v1.2.3