| author | Walther Neuper <neuper@ist.tugraz.at> |
| Fri, 01 Oct 2010 17:27:55 +0200 | |
| branch | isac-update-Isa09-2 |
| changeset 38039 | 99cb0d80ff32 |
| parent 27572 | 67cd6ed76446 |
| child 39406 | 0dec18004e75 |
| permissions | -rw-r--r-- |
| wenzelm@7355 | 1 |
|
| wenzelm@7355 | 2 |
(** Applying HypsubstFun to generate hyp_subst_tac **) |
| wenzelm@7355 | 3 |
structure Hypsubst_Data = |
| haftmann@20974 | 4 |
struct |
| wenzelm@7355 | 5 |
structure Simplifier = Simplifier |
| wenzelm@21218 | 6 |
val dest_eq = FOLogic.dest_eq |
| wenzelm@7355 | 7 |
val dest_Trueprop = FOLogic.dest_Trueprop |
| wenzelm@7355 | 8 |
val dest_imp = FOLogic.dest_imp |
| wenzelm@21539 | 9 |
val eq_reflection = thm "eq_reflection" |
| wenzelm@21539 | 10 |
val rev_eq_reflection = thm "meta_eq_to_obj_eq" |
| wenzelm@21539 | 11 |
val imp_intr = thm "impI" |
| wenzelm@21539 | 12 |
val rev_mp = thm "rev_mp" |
| wenzelm@21539 | 13 |
val subst = thm "subst" |
| wenzelm@21539 | 14 |
val sym = thm "sym" |
| wenzelm@21539 | 15 |
val thin_refl = thm "thin_refl" |
| krauss@27572 | 16 |
val prop_subst = @{lemma "PROP P(t) ==> PROP prop (x = t ==> PROP P(x))"
|
| krauss@27572 | 17 |
by (unfold prop_def) (drule eq_reflection, unfold)} |
| haftmann@20974 | 18 |
end; |
| wenzelm@7355 | 19 |
|
| wenzelm@7355 | 20 |
structure Hypsubst = HypsubstFun(Hypsubst_Data); |
| wenzelm@7355 | 21 |
open Hypsubst; |