forked from JacquesCarette/hol-light-qe
-
Notifications
You must be signed in to change notification settings - Fork 0
/
holQE.ml
18 lines (13 loc) · 890 Bytes
/
holQE.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
(* ========================================================================= *)
(* HOL LIGHT QE *)
(* ========================================================================= *)
(* ------------------------------------------------------------------------- *)
(* Implementation of basic QE constants *)
(* ------------------------------------------------------------------------- *)
loads "Constructions/epsilon.ml";;
(* ------------------------------------------------------------------------- *)
(* General QE tactics *)
(* ------------------------------------------------------------------------- *)
loads "Constructions/gen_tactics.ml";;
loads "Constructions/QuotationTactics.ml";;
loads "Constructions/ConstructionTactics.ml";;