923

1 

7357

2 
structure HOL =


3 
struct


4 
val thy = the_context ();


5 
val plusI = plusI;


6 
val minusI = minusI;


7 
val timesI = timesI;


8 
val powerI = powerI;


9 
val eq_reflection = eq_reflection;


10 
val refl = refl;


11 
val subst = subst;


12 
val ext = ext;


13 
val selectI = selectI;


14 
val impI = impI;


15 
val mp = mp;


16 
val True_def = True_def;


17 
val All_def = All_def;


18 
val Ex_def = Ex_def;


19 
val False_def = False_def;


20 
val not_def = not_def;


21 
val and_def = and_def;


22 
val or_def = or_def;


23 
val Ex1_def = Ex1_def;


24 
val iff = iff;


25 
val True_or_False = True_or_False;


26 
val Let_def = Let_def;


27 
val if_def = if_def;


28 
val arbitrary_def = arbitrary_def;

3621

29 
end;

5888

30 

7529

31 
AddXIs [disjI1, disjI2];


32 

7357

33 
open HOL;
