diff options
| author |  mark <> | 2012-02-24 12:07:26 +0000 |
|---|---|---|
| committer | mark <> | 2012-02-24 12:07:26 +0000 |
| commit | cf0c3e813e4601f7462268703efd5b14424bd6c3 (patch) | |
| tree | 5ed504ddfb01b33857d9d235c35787e7f996fc54 /hol-light/TacticRecording/examples1.ml | |
| parent | 4ed83bcb88f220cc08c3223bd4f274eaa5f31e0c (diff) | |
Remove option aspect of 'finfo' datatype, and rename datatype to 'mldata'.
Add wrapper function for :thm -> thm list.
Promote more objects.
Diffstat (limited to 'hol-light/TacticRecording/examples1.ml')
| -rw-r--r-- | hol-light/TacticRecording/examples1.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/hol-light/TacticRecording/examples1.ml b/hol-light/TacticRecording/examples1.ml index fd0b446c..4e67ca18 100644 --- a/hol-light/TacticRecording/examples1.ml +++ b/hol-light/TacticRecording/examples1.ml @@ -43,8 +43,6 @@ g `(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`;; e (REPEAT CONJ_TAC THEN GEN_TAC THEN REFL_TAC);; let th = top_thm ();; -#use"TacticRecording/mlexport.ml";; - print_executed_proof true;; print_flat_proof true;; print_thenl_proof ();; |