diff options
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";; |