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
     1 
     2 (** Applying HypsubstFun to generate hyp_subst_tac **)
     3 structure Hypsubst_Data =
     4 struct
     5   structure Simplifier = Simplifier
     6   val dest_eq = FOLogic.dest_eq
     7   val dest_Trueprop = FOLogic.dest_Trueprop
     8   val dest_imp = FOLogic.dest_imp
     9   val eq_reflection = thm "eq_reflection"
    10   val rev_eq_reflection = thm "meta_eq_to_obj_eq"
    11   val imp_intr = thm "impI"
    12   val rev_mp = thm "rev_mp"
    13   val subst = thm "subst"
    14   val sym = thm "sym"
    15   val thin_refl = thm "thin_refl"
    16   val prop_subst = @{lemma "PROP P(t) ==> PROP prop (x = t ==> PROP P(x))"
    17                      by (unfold prop_def) (drule eq_reflection, unfold)}
    18 end;
    19 
    20 structure Hypsubst = HypsubstFun(Hypsubst_Data);
    21 open Hypsubst;