|
7355
|
1 |
|
|
|
2 |
(** Applying HypsubstFun to generate hyp_subst_tac **)
|
|
|
3 |
structure Hypsubst_Data =
|
|
20974
|
4 |
struct
|
|
7355
|
5 |
structure Simplifier = Simplifier
|
|
21218
|
6 |
val dest_eq = FOLogic.dest_eq
|
|
7355
|
7 |
val dest_Trueprop = FOLogic.dest_Trueprop
|
|
|
8 |
val dest_imp = FOLogic.dest_imp
|
|
21539
|
9 |
val eq_reflection = thm "eq_reflection"
|
|
|
10 |
val rev_eq_reflection = thm "meta_eq_to_obj_eq"
|
|
|
11 |
val imp_intr = thm "impI"
|
|
|
12 |
val rev_mp = thm "rev_mp"
|
|
|
13 |
val subst = thm "subst"
|
|
|
14 |
val sym = thm "sym"
|
|
|
15 |
val thin_refl = thm "thin_refl"
|
|
20974
|
16 |
end;
|
|
7355
|
17 |
|
|
|
18 |
structure Hypsubst = HypsubstFun(Hypsubst_Data);
|
|
|
19 |
open Hypsubst;
|