|
7355
|
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;
|