Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned hypsubst setup;
authorwenzelm
Tue, 07 Nov 2006 14:29:57 +0100
changeset 21218 38013c3a77a2
parent 21217 0425fc57510f
child 21219 e1063a0e6dfd
tuned hypsubst setup;
src/FOL/hypsubstdata.ML file | annotate | diff | comparison | revisions
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- a/src/FOL/hypsubstdata.ML	Tue Nov 07 14:14:36 2006 +0100
+++ b/src/FOL/hypsubstdata.ML	Tue Nov 07 14:29:57 2006 +0100
@@ -3,7 +3,7 @@
 structure Hypsubst_Data =
 struct
   structure Simplifier = Simplifier
-  fun dest_eq (Const("op =",T) $ t $ u) = ((t, u), domain_type T)
+  val dest_eq = FOLogic.dest_eq
   val dest_Trueprop = FOLogic.dest_Trueprop
   val dest_imp = FOLogic.dest_imp
   val eq_reflection = eq_reflection
--- a/src/HOL/HOL.thy	Tue Nov 07 14:14:36 2006 +0100
+++ b/src/HOL/HOL.thy	Tue Nov 07 14:29:57 2006 +0100
@@ -864,7 +864,7 @@
 structure Hypsubst = HypsubstFun(
 struct
   structure Simplifier = Simplifier
-  val dest_eq = HOLogic.dest_eq_typ
+  val dest_eq = HOLogic.dest_eq
   val dest_Trueprop = HOLogic.dest_Trueprop
   val dest_imp = HOLogic.dest_imp
   val eq_reflection = HOL.eq_reflection
isabelle