|
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;
|
|
|
15 |
val impI = impI;
|
|
|
16 |
val mp = mp;
|
|
|
17 |
val True_def = True_def;
|
|
|
18 |
val All_def = All_def;
|
|
|
19 |
val Ex_def = Ex_def;
|
|
|
20 |
val False_def = False_def;
|
|
|
21 |
val not_def = not_def;
|
|
|
22 |
val and_def = and_def;
|
|
|
23 |
val or_def = or_def;
|
|
|
24 |
val Ex1_def = Ex1_def;
|
|
|
25 |
val iff = iff;
|
|
|
26 |
val True_or_False = True_or_False;
|
|
|
27 |
val Let_def = Let_def;
|
|
|
28 |
val if_def = if_def;
|
|
|
29 |
val arbitrary_def = arbitrary_def;
|
|
3621
|
30 |
end;
|
|
5888
|
31 |
|
|
11588
|
32 |
AddXIs [equal_intr_rule, ext];
|
|
|
33 |
AddXEs [disjI1, disjI2, ex1_implies_ex, sym];
|
|
7529
|
34 |
|
|
7357
|
35 |
open HOL;
|
|
11749
|
36 |
|
|
|
37 |
val Least_def = thm "Least_def";
|
|
|
38 |
val Least_equality = thm "Least_equality";
|
|
|
39 |
val mono_def = thm "mono_def";
|
|
|
40 |
val monoI = thm "monoI";
|
|
|
41 |
val monoD = thm "monoD";
|
|
|
42 |
val min_def = thm "min_def";
|
|
|
43 |
val min_of_mono = thm "min_of_mono";
|
|
|
44 |
val max_def = thm "max_def";
|
|
|
45 |
val max_of_mono = thm "max_of_mono";
|
|
|
46 |
val min_leastL = thm "min_leastL";
|
|
|
47 |
val max_leastL = thm "max_leastL";
|
|
|
48 |
val min_leastR = thm "min_leastR";
|
|
|
49 |
val max_leastR = thm "max_leastR";
|
|
|
50 |
val order_eq_refl = thm "order_eq_refl";
|
|
|
51 |
val order_less_irrefl = thm "order_less_irrefl";
|
|
|
52 |
val order_le_less = thm "order_le_less";
|
|
|
53 |
val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq";
|
|
|
54 |
val order_less_imp_le = thm "order_less_imp_le";
|
|
|
55 |
val order_less_not_sym = thm "order_less_not_sym";
|
|
|
56 |
val order_less_asym = thm "order_less_asym";
|
|
|
57 |
val order_less_trans = thm "order_less_trans";
|
|
|
58 |
val order_le_less_trans = thm "order_le_less_trans";
|
|
|
59 |
val order_less_le_trans = thm "order_less_le_trans";
|
|
|
60 |
val order_less_imp_not_less = thm "order_less_imp_not_less";
|
|
|
61 |
val order_less_imp_triv = thm "order_less_imp_triv";
|
|
|
62 |
val order_less_imp_not_eq = thm "order_less_imp_not_eq";
|
|
|
63 |
val order_less_imp_not_eq2 = thm "order_less_imp_not_eq2";
|
|
|
64 |
val linorder_less_linear = thm "linorder_less_linear";
|
|
|
65 |
val linorder_cases = thm "linorder_cases";
|
|
|
66 |
val linorder_not_less = thm "linorder_not_less";
|
|
|
67 |
val linorder_not_le = thm "linorder_not_le";
|
|
|
68 |
val linorder_neq_iff = thm "linorder_neq_iff";
|
|
|
69 |
val linorder_neqE = thm "linorder_neqE";
|
|
|
70 |
val min_same = thm "min_same";
|
|
|
71 |
val max_same = thm "max_same";
|
|
|
72 |
val le_max_iff_disj = thm "le_max_iff_disj";
|
|
|
73 |
val le_maxI1 = thm "le_maxI1";
|
|
|
74 |
val le_maxI2 = thm "le_maxI2";
|
|
|
75 |
val less_max_iff_disj = thm "less_max_iff_disj";
|
|
|
76 |
val max_le_iff_conj = thm "max_le_iff_conj";
|
|
|
77 |
val max_less_iff_conj = thm "max_less_iff_conj";
|
|
|
78 |
val le_min_iff_conj = thm "le_min_iff_conj";
|
|
|
79 |
val min_less_iff_conj = thm "min_less_iff_conj";
|
|
|
80 |
val min_le_iff_disj = thm "min_le_iff_disj";
|
|
|
81 |
val min_less_iff_disj = thm "min_less_iff_disj";
|
|
|
82 |
val split_min = thm "split_min";
|
|
|
83 |
val split_max = thm "split_max";
|
|
|
84 |
val order_refl = thm "order_refl";
|
|
|
85 |
val order_trans = thm "order_trans";
|
|
|
86 |
val order_antisym = thm "order_antisym";
|
|
|
87 |
val order_less_le = thm "order_less_le";
|
|
|
88 |
val linorder_linear = thm "linorder_linear";
|