src/FOL/hypsubstdata.ML
author wenzelm
Mon Sep 06 19:13:10 2010 +0200 (2010-09-06)
changeset 39159 0dec18004e75
parent 27572 67cd6ed76446
child 39782 f75381bc46d2
permissions -rw-r--r--
more antiquotations;
     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;