equal
deleted
inserted
replaced
11 val Exh_tr = thm "Exh_tr"; |
11 val Exh_tr = thm "Exh_tr"; |
12 val trE = thm "trE"; |
12 val trE = thm "trE"; |
13 val tr_defs = thms "tr_defs"; |
13 val tr_defs = thms "tr_defs"; |
14 val dist_less_tr = thms "dist_less_tr"; |
14 val dist_less_tr = thms "dist_less_tr"; |
15 val dist_eq_tr = thms "dist_eq_tr"; |
15 val dist_eq_tr = thms "dist_eq_tr"; |
16 val ifte_simp = thm "ifte_simp"; |
|
17 val ifte_thms = thms "ifte_thms"; |
16 val ifte_thms = thms "ifte_thms"; |
18 val andalso_thms = thms "andalso_thms"; |
17 val andalso_thms = thms "andalso_thms"; |
19 val orelse_thms = thms "orelse_thms"; |
18 val orelse_thms = thms "orelse_thms"; |
20 val neg_thms = thms "neg_thms"; |
19 val neg_thms = thms "neg_thms"; |
21 val split_If2 = thm "split_If2"; |
20 val split_If2 = thm "split_If2"; |