19 (mk_solver' "adm_tac" (fn ss => |
19 (mk_solver' "adm_tac" (fn ss => |
20 Adm.adm_tac (Simplifier.the_context ss) |
20 Adm.adm_tac (Simplifier.the_context ss) |
21 (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)))); |
21 (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)))); |
22 *} |
22 *} |
23 |
23 |
|
24 text {* Legacy theorem names *} |
|
25 |
|
26 lemmas sq_ord_less_eq_trans = below_eq_trans |
|
27 lemmas sq_ord_eq_less_trans = eq_below_trans |
|
28 lemmas refl_less = below_refl |
|
29 lemmas trans_less = below_trans |
|
30 lemmas antisym_less = below_antisym |
|
31 lemmas antisym_less_inverse = below_antisym_inverse |
|
32 lemmas box_less = box_below |
|
33 lemmas rev_trans_less = rev_below_trans |
|
34 lemmas not_less2not_eq = not_below2not_eq |
|
35 lemmas less_UU_iff = below_UU_iff |
|
36 lemmas flat_less_iff = flat_below_iff |
|
37 lemmas adm_less = adm_below |
|
38 lemmas adm_not_less = adm_not_below |
|
39 lemmas adm_compact_not_less = adm_compact_not_below |
|
40 lemmas less_fun_def = below_fun_def |
|
41 lemmas expand_fun_less = expand_fun_below |
|
42 lemmas less_fun_ext = below_fun_ext |
|
43 lemmas less_discr_def = below_discr_def |
|
44 lemmas discr_less_eq = discr_below_eq |
|
45 lemmas less_unit_def = below_unit_def |
|
46 lemmas less_cprod_def = below_prod_def |
|
47 lemmas prod_lessI = prod_belowI |
|
48 lemmas Pair_less_iff = Pair_below_iff |
|
49 lemmas fst_less_iff = fst_below_iff |
|
50 lemmas snd_less_iff = snd_below_iff |
|
51 lemmas expand_cfun_less = expand_cfun_below |
|
52 lemmas less_cfun_ext = below_cfun_ext |
|
53 lemmas injection_less = injection_below |
|
54 lemmas approx_less = approx_below |
|
55 lemmas profinite_less_ext = profinite_below_ext |
|
56 lemmas less_up_def = below_up_def |
|
57 lemmas not_Iup_less = not_Iup_below |
|
58 lemmas Iup_less = Iup_below |
|
59 lemmas up_less = up_below |
|
60 lemmas cpair_less = cpair_below |
|
61 lemmas less_cprod = below_cprod |
|
62 lemmas cfst_less_iff = cfst_below_iff |
|
63 lemmas csnd_less_iff = csnd_below_iff |
|
64 lemmas Def_inject_less_eq = Def_below_Def |
|
65 lemmas Def_less_is_eq = Def_below_iff |
|
66 lemmas spair_less_iff = spair_below_iff |
|
67 lemmas less_sprod = below_sprod |
|
68 lemmas spair_less = spair_below |
|
69 lemmas sfst_less_iff = sfst_below_iff |
|
70 lemmas ssnd_less_iff = ssnd_below_iff |
|
71 lemmas fix_least_less = fix_least_below |
|
72 lemmas dist_less_one = dist_below_one |
|
73 lemmas less_ONE = below_ONE |
|
74 lemmas ONE_less_iff = ONE_below_iff |
|
75 lemmas less_sinlD = below_sinlD |
|
76 lemmas less_sinrD = below_sinrD |
|
77 |
24 end |
78 end |