author | wenzelm |
Wed, 06 Dec 2006 01:12:43 +0100 | |
changeset 21672 | 29c346b165d4 |
parent 21670 | 704510b508ef |
child 22218 | 30a8890d2967 |
permissions | -rw-r--r-- |
21670
704510b508ef
reduced to genuine legacy bindings -- others in HOL.thy;
wenzelm
parents:
21619
diff
changeset
|
1 |
(* |
704510b508ef
reduced to genuine legacy bindings -- others in HOL.thy;
wenzelm
parents:
21619
diff
changeset
|
2 |
ID: $Id$ |
704510b508ef
reduced to genuine legacy bindings -- others in HOL.thy;
wenzelm
parents:
21619
diff
changeset
|
3 |
*) |
21546 | 4 |
|
21670
704510b508ef
reduced to genuine legacy bindings -- others in HOL.thy;
wenzelm
parents:
21619
diff
changeset
|
5 |
(** legacy ML bindings **) |
12999 | 6 |
|
21619 | 7 |
val all_conj_distrib = thm "all_conj_distrib"; |
8 |
val all_simps = thms "all_simps"; |
|
9 |
val atomize_not = thm "atomize_not"; |
|
10 |
val case_split = thm "case_split_thm"; |
|
11 |
val case_split_thm = thm "case_split_thm" |
|
12 |
val cases_simp = thm "cases_simp"; |
|
13 |
val choice_eq = thm "choice_eq" |
|
14 |
val cong = thm "cong" |
|
15 |
val conj_comms = thms "conj_comms"; |
|
16 |
val conj_cong = thm "conj_cong"; |
|
17 |
val def_imp_eq = thm "def_imp_eq"; |
|
20944 | 18 |
val de_Morgan_conj = thm "de_Morgan_conj"; |
19 |
val de_Morgan_disj = thm "de_Morgan_disj"; |
|
20 |
val disj_assoc = thm "disj_assoc"; |
|
21619 | 21 |
val disj_comms = thms "disj_comms"; |
22 |
val disj_cong = thm "disj_cong"; |
|
23 |
val eq_ac = thms "eq_ac"; |
|
24 |
val eq_cong2 = thm "eq_cong2" |
|
25 |
val Eq_FalseI = thm "Eq_FalseI"; |
|
26 |
val Eq_TrueI = thm "Eq_TrueI"; |
|
27 |
val Ex1_def = thm "Ex1_def" |
|
28 |
val ex_disj_distrib = thm "ex_disj_distrib"; |
|
29 |
val ex_simps = thms "ex_simps"; |
|
20944 | 30 |
val if_cancel = thm "if_cancel"; |
31 |
val if_eq_cancel = thm "if_eq_cancel"; |
|
21619 | 32 |
val if_False = thm "if_False"; |
20944 | 33 |
val iff_conv_conj_imp = thm "iff_conv_conj_imp"; |
21619 | 34 |
val iff = thm "iff" |
35 |
val if_splits = thms "if_splits"; |
|
36 |
val if_True = thm "if_True"; |
|
37 |
val if_weak_cong = thm "if_weak_cong" |
|
38 |
val imp_all = thm "imp_all"; |
|
20944 | 39 |
val imp_cong = thm "imp_cong"; |
21619 | 40 |
val imp_conjL = thm "imp_conjL"; |
41 |
val imp_conjR = thm "imp_conjR"; |
|
20944 | 42 |
val imp_conv_disj = thm "imp_conv_disj"; |
43 |
val simp_implies_def = thm "simp_implies_def"; |
|
21619 | 44 |
val simp_thms = thms "simp_thms"; |
45 |
val split_if = thm "split_if"; |
|
46 |
val the1_equality = thm "the1_equality" |
|
47 |
val theI = thm "theI" |
|
48 |
val theI' = thm "theI'" |
|
20944 | 49 |
val True_implies_equals = thm "True_implies_equals"; |