blob: bfdc1488d1eed6118bb3927f60c6a03ecc66e5ff (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
(* Library stuff *)
#use "TacticRecording/lib.ml";;
#use "TacticRecording/dltree.mli";;
#use "TacticRecording/dltree.ml";;
(* Datatypes and recording mechanism *)
#use "TacticRecording/xthm.ml";;
#use "TacticRecording/xtactics.ml";;
#use "TacticRecording/tacticrec.ml";;
#use "TacticRecording/wrappers.ml";;
(* Prooftree support *)
#use "TacticRecording/prooftree.ml";;
(* 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 *)
#use "TacticRecording/promote.ml";;
|
