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