diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-23 18:04:40 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-23 18:04:40 +0000 |
| commit | 1f47fa17959174e05904eae19abd4c23930d56ff (patch) | |
| tree | 07fc5511f72c28eaa5c038a6001759aa3653aff1 /hol98 | |
| parent | 01c1cd0d06886221bae44a244b9b8f53d48e1a7a (diff) | |
Comment
Diffstat (limited to 'hol98')
| -rw-r--r-- | hol98/example.sml | 5 |
1 files 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 |