author | huffman |
Thu, 03 Nov 2005 00:12:29 +0100 | |
changeset 18070 | b653e18f0a41 |
parent 16922 | 2128ac2aa5db |
permissions | -rw-r--r-- |
2640 | 1 |
|
15649 | 2 |
(* legacy ML bindings *) |
2640 | 3 |
|
16922 | 4 |
val andalso_and = thm "andalso_and"; |
15649 | 5 |
val andalso_def = thm "andalso_def"; |
16922 | 6 |
val andalso_or = thm "andalso_or"; |
15649 | 7 |
val andalso_thms = thms "andalso_thms"; |
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16922
diff
changeset
|
8 |
val compact_FF = thm "compact_FF"; |
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16922
diff
changeset
|
9 |
val compact_TT = thm "compact_TT"; |
15649 | 10 |
val Def_bool1 = thm "Def_bool1"; |
11 |
val Def_bool2 = thm "Def_bool2"; |
|
12 |
val Def_bool3 = thm "Def_bool3"; |
|
13 |
val Def_bool4 = thm "Def_bool4"; |
|
16922 | 14 |
val dist_eq_tr = thms "dist_eq_tr"; |
15 |
val dist_less_tr = thms "dist_less_tr"; |
|
16 |
val Exh_tr = thm "Exh_tr"; |
|
17 |
val FF_def = thm "FF_def"; |
|
18 |
val If2_def = thm "If2_def"; |
|
15649 | 19 |
val If_and_if = thm "If_and_if"; |
16922 | 20 |
val ifte_def = thm "ifte_def"; |
21 |
val ifte_thms = thms "ifte_thms"; |
|
22 |
val neg_def = thm "neg_def"; |
|
23 |
val neg_thms = thms "neg_thms"; |
|
24 |
val orelse_def = thm "orelse_def"; |
|
25 |
val orelse_thms = thms "orelse_thms"; |
|
26 |
val split_If2 = thm "split_If2"; |
|
27 |
val tr_defs = thms "tr_defs"; |
|
28 |
val trE = thm "trE"; |
|
29 |
val TT_def = thm "TT_def"; |