author | paulson |
Mon, 25 Jun 2001 15:36:55 +0200 | |
changeset 11378 | 5c84a5ca3a21 |
parent 10433 | 6c5659d461dd |
child 11451 | 8abfb4f7bd02 |
permissions | -rw-r--r-- |
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 eq_reflection = eq_reflection; |
|
12 |
val refl = refl; |
|
13 |
val subst = subst; |
|
14 |
val ext = ext; |
|
9970 | 15 |
val someI = someI; |
7357 | 16 |
val impI = impI; |
17 |
val mp = mp; |
|
18 |
val True_def = True_def; |
|
19 |
val All_def = All_def; |
|
20 |
val Ex_def = Ex_def; |
|
21 |
val False_def = False_def; |
|
22 |
val not_def = not_def; |
|
23 |
val and_def = and_def; |
|
24 |
val or_def = or_def; |
|
25 |
val Ex1_def = Ex1_def; |
|
26 |
val iff = iff; |
|
27 |
val True_or_False = True_or_False; |
|
28 |
val Let_def = Let_def; |
|
29 |
val if_def = if_def; |
|
30 |
val arbitrary_def = arbitrary_def; |
|
3621 | 31 |
end; |
5888 | 32 |
|
10062 | 33 |
AddXIs [equal_intr_rule, disjI1, disjI2, ext]; |
10273
59570adf2d3c
declare sym [elim?] in HOL.ML instead of Calculation.thy;
wenzelm
parents:
10182
diff
changeset
|
34 |
AddXEs [ex1_implies_ex, someI_ex, sym]; |
7529 | 35 |
|
7357 | 36 |
open HOL; |