equal
deleted
inserted
replaced
1 |
1 |
2 (* legacy ML bindings *) |
2 (* legacy ML bindings *) |
3 |
3 |
4 val adm_nFF = thm "adm_nFF"; |
|
5 val adm_nTT = thm "adm_nTT"; |
|
6 val adm_trick_1 = thm "adm_trick_1"; |
|
7 val adm_trick_2 = thm "adm_trick_2"; |
|
8 val adm_tricks = thms "adm_tricks"; |
|
9 val andalso_and = thm "andalso_and"; |
4 val andalso_and = thm "andalso_and"; |
10 val andalso_def = thm "andalso_def"; |
5 val andalso_def = thm "andalso_def"; |
11 val andalso_or = thm "andalso_or"; |
6 val andalso_or = thm "andalso_or"; |
12 val andalso_thms = thms "andalso_thms"; |
7 val andalso_thms = thms "andalso_thms"; |
|
8 val compact_FF = thm "compact_FF"; |
|
9 val compact_TT = thm "compact_TT"; |
13 val Def_bool1 = thm "Def_bool1"; |
10 val Def_bool1 = thm "Def_bool1"; |
14 val Def_bool2 = thm "Def_bool2"; |
11 val Def_bool2 = thm "Def_bool2"; |
15 val Def_bool3 = thm "Def_bool3"; |
12 val Def_bool3 = thm "Def_bool3"; |
16 val Def_bool4 = thm "Def_bool4"; |
13 val Def_bool4 = thm "Def_bool4"; |
17 val dist_eq_tr = thms "dist_eq_tr"; |
14 val dist_eq_tr = thms "dist_eq_tr"; |