diff options
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 ();; |