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