src/FOL/hypsubstdata.ML
author wenzelm
Fri, 06 May 2011 20:25:41 +0200
changeset 42712 574613b47583
parent 39782 f75381bc46d2
permissions -rw-r--r--
no need for underscore.sty -- latex.ltx provides \textunderscore and \_ already;


(** 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}
end;

structure Hypsubst = HypsubstFun(Hypsubst_Data);
open Hypsubst;