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.
because intT is now defined in HOLogic
authorpaulson
Fri, 23 Jul 1999 17:28:18 +0200
changeset 7076 a30e024791c6
parent 7075 5ba8d1e42ca6
child 7077 60b098bb8b8a
because intT is now defined in HOLogic
src/HOL/Integ/simproc.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/simproc.ML	Fri Jul 23 17:27:48 1999 +0200
+++ b/src/HOL/Integ/simproc.ML	Fri Jul 23 17:28:18 1999 +0200
@@ -31,7 +31,7 @@
   val eq_reflection	= eq_reflection
 
   val thy	= IntDef.thy
-  val T		= Type ("IntDef.int", [])
+  val T		= HOLogic.intT
   val zero	= Const ("IntDef.int", HOLogic.natT --> T) $ HOLogic.zero
   val add_cancel_21	= zadd_cancel_21
   val add_cancel_end	= zadd_cancel_end
isabelle