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


(** Applying HypsubstFun to generate hyp_subst_tac **)
structure Hypsubst_Data =
struct
  structure Simplifier = Simplifier
  val dest_eq = FOLogic.dest_eq
  val dest_Trueprop = FOLogic.dest_Trueprop
  val dest_imp = FOLogic.dest_imp
  val eq_reflection = thm "eq_reflection"
  val rev_eq_reflection = thm "meta_eq_to_obj_eq"
  val imp_intr = thm "impI"
  val rev_mp = thm "rev_mp"
  val subst = thm "subst"
  val sym = thm "sym"
  val thin_refl = thm "thin_refl"
  val prop_subst = @{lemma "PROP P(t) ==> PROP prop (x = t ==> PROP P(x))"
                     by (unfold prop_def) (drule eq_reflection, unfold)}
end;

structure Hypsubst = HypsubstFun(Hypsubst_Data);
open Hypsubst;