author  wenzelm 
Thu, 19 Oct 2000 21:20:53 +0200  
changeset 10273  59570adf2d3c 
parent 10182  5413bcce1482 
child 10433  6c5659d461dd 
permissions  rwrr 
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]; 
10273
59570adf2d3c
declare sym [elim?] in HOL.ML instead of Calculation.thy;
wenzelm
parents:
10182
diff
changeset

35 
AddXEs [ex1_implies_ex, someI_ex, sym]; 
7529  36 

7357  37 
open HOL; 