equal
deleted
inserted
replaced
26 |
26 |
27 (** Applying HypsubstFun to generate hyp_subst_tac **) |
27 (** Applying HypsubstFun to generate hyp_subst_tac **) |
28 structure Hypsubst_Data = |
28 structure Hypsubst_Data = |
29 struct |
29 struct |
30 structure Simplifier = Simplifier |
30 structure Simplifier = Simplifier |
31 (*Take apart an equality judgement; otherwise raise Match!*) |
31 (*These destructors Match!*) |
32 fun dest_eq (Const("Trueprop",_) $ (Const("op =",T) $ t $ u)) = |
32 fun dest_eq (Const("op =",T) $ t $ u) = (t, u, domain_type T) |
33 (t, u, domain_type T) |
33 val dest_Trueprop = FOLogic.dest_Trueprop |
|
34 val dest_imp = FOLogic.dest_imp |
34 val eq_reflection = eq_reflection |
35 val eq_reflection = eq_reflection |
35 val imp_intr = impI |
36 val imp_intr = impI |
36 val rev_mp = rev_mp |
37 val rev_mp = rev_mp |
37 val subst = subst |
38 val subst = subst |
38 val sym = sym |
39 val sym = sym |