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/main.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/main.ml')
| -rw-r--r-- | hol-light/TacticRecording/main.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/hol-light/TacticRecording/main.ml b/hol-light/TacticRecording/main.ml index bfdc1488..57c82547 100644 --- a/hol-light/TacticRecording/main.ml +++ b/hol-light/TacticRecording/main.ml @@ -6,6 +6,7 @@ (* Datatypes and recording mechanism *) +#use "TacticRecording/mldata.ml";; #use "TacticRecording/xthm.ml";; #use "TacticRecording/xtactics.ml";; #use "TacticRecording/tacticrec.ml";; |