equal
deleted
inserted
replaced
1 |
|
2 (** Applying HypsubstFun to generate hyp_subst_tac **) |
|
3 structure Hypsubst_Data = |
|
4 struct |
|
5 structure Simplifier = Simplifier |
|
6 val dest_eq = FOLogic.dest_eq |
|
7 val dest_Trueprop = FOLogic.dest_Trueprop |
|
8 val dest_imp = FOLogic.dest_imp |
|
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} |
|
16 end; |
|
17 |
|
18 structure Hypsubst = HypsubstFun(Hypsubst_Data); |
|
19 open Hypsubst; |
|