src/FOL/hypsubstdata.ML
changeset 7355 4c43090659ca
child 9528 95852b4be214
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/hypsubstdata.ML	Wed Aug 25 20:45:19 1999 +0200
@@ -0,0 +1,20 @@
+
+(** Applying HypsubstFun to generate hyp_subst_tac **)
+structure Hypsubst_Data =
+  struct
+  structure Simplifier = Simplifier
+    (*These destructors  Match!*)
+  fun dest_eq (Const("op =",T)  $ t $ u) = (t, u, domain_type T)
+  val dest_Trueprop = FOLogic.dest_Trueprop
+  val dest_imp = FOLogic.dest_imp
+  val eq_reflection = eq_reflection
+  val imp_intr = impI
+  val rev_mp = rev_mp
+  val subst = subst
+  val sym = sym
+  val thin_refl = prove_goal (the_context ())
+		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
+  end;
+
+structure Hypsubst = HypsubstFun(Hypsubst_Data);
+open Hypsubst;