diff options
| author |  mark <> | 2012-02-23 11:00:45 +0000 |
|---|---|---|
| committer | mark <> | 2012-02-23 11:00:45 +0000 |
| commit | 448583e76767da575c9d90f54266d434c86282ed (patch) | |
| tree | f62d7cbd6b00c9d894929d37ff261efbd7b11916 /hol-light/TacticRecording/main.ml | |
| parent | 6ecd3be998c4d2a6d8dae8ec2f67c50305a251ef (diff) | |
Capability for exporting .dot files added.
Diffstat (limited to 'hol-light/TacticRecording/main.ml')
| -rw-r--r-- | hol-light/TacticRecording/main.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/hol-light/TacticRecording/main.ml b/hol-light/TacticRecording/main.ml index 44c01951..bfdc1488 100644 --- a/hol-light/TacticRecording/main.ml +++ b/hol-light/TacticRecording/main.ml @@ -15,9 +15,14 @@ #use "TacticRecording/prooftree.ml";; -(* Hiproofs, refactoring and export *) +(* Hiproofs & refactoring *) #use "TacticRecording/hiproofs.ml";; + +(* Export *) + +#use "TacticRecording/printutils.ml";; +#use "TacticRecording/gvexport.ml";; #use "TacticRecording/mlexport.ml";; (* Overwriting the existing HOL Light objects *) |