src/FOL/hypsubstdata.ML
author krauss
Mon Jul 14 17:47:18 2008 +0200 (2008-07-14)
changeset 27572 67cd6ed76446
parent 21539 c5cf9243ad62
child 39159 0dec18004e75
permissions -rw-r--r--
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
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;