10011

1 
(* Title: HOL/HOL.ML


2 
ID: $Id$


3 
*)


4 

7357

5 
structure HOL =


6 
struct


7 
val thy = the_context ();


8 
val plusI = plusI;


9 
val minusI = minusI;


10 
val timesI = timesI;


11 
val powerI = powerI;


12 
val eq_reflection = eq_reflection;


13 
val refl = refl;


14 
val subst = subst;


15 
val ext = ext;

9970

16 
val someI = someI;

7357

17 
val impI = impI;


18 
val mp = mp;


19 
val True_def = True_def;


20 
val All_def = All_def;


21 
val Ex_def = Ex_def;


22 
val False_def = False_def;


23 
val not_def = not_def;


24 
val and_def = and_def;


25 
val or_def = or_def;


26 
val Ex1_def = Ex1_def;


27 
val iff = iff;


28 
val True_or_False = True_or_False;


29 
val Let_def = Let_def;


30 
val if_def = if_def;


31 
val arbitrary_def = arbitrary_def;

3621

32 
end;

5888

33 

10062

34 
AddXIs [equal_intr_rule, disjI1, disjI2, ext];

10182

35 
AddXEs [ex1_implies_ex, someI_ex];

7529

36 

7357

37 
open HOL;
