equal
deleted
inserted
replaced
|
1 |
|
2 (** Applying HypsubstFun to generate hyp_subst_tac **) |
|
3 structure Hypsubst_Data = |
|
4 struct |
|
5 structure Simplifier = Simplifier |
|
6 (*These destructors Match!*) |
|
7 fun dest_eq (Const("op =",T) $ t $ u) = (t, u, domain_type T) |
|
8 val dest_Trueprop = FOLogic.dest_Trueprop |
|
9 val dest_imp = FOLogic.dest_imp |
|
10 val eq_reflection = eq_reflection |
|
11 val imp_intr = impI |
|
12 val rev_mp = rev_mp |
|
13 val subst = subst |
|
14 val sym = sym |
|
15 val thin_refl = prove_goal (the_context ()) |
|
16 "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]); |
|
17 end; |
|
18 |
|
19 structure Hypsubst = HypsubstFun(Hypsubst_Data); |
|
20 open Hypsubst; |