diff options
Diffstat (limited to 'hol-light/TacticRecording/examples1.ml')
| -rw-r--r-- | hol-light/TacticRecording/examples1.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/hol-light/TacticRecording/examples1.ml b/hol-light/TacticRecording/examples1.ml index b587c18f..fd0b446c 100644 --- a/hol-light/TacticRecording/examples1.ml +++ b/hol-light/TacticRecording/examples1.ml @@ -45,10 +45,11 @@ let th = top_thm ();; #use"TacticRecording/mlexport.ml";; -print_executed_proof ();; -print_flat_proof ();; +print_executed_proof true;; +print_flat_proof true;; print_thenl_proof ();; -print_optimal_proof ();; +print_packaged_proof ();; +print_gv_proof ();; g `(y:A) = z ==> (x:A) = x /\ y = y /\ z = z`;; e (STRIP_TAC);; |