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.
explicit import of Datatype.thy due to hook bootstrap problem
authorhaftmann
Thu, 10 May 2007 10:21:48 +0200
changeset 22919 3de2d0b5b89a
parent 22918 b8b4d53ccd24
child 22920 0dbcb73bf9bf
explicit import of Datatype.thy due to hook bootstrap problem
src/HOL/FunDef.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/FunDef.thy	Thu May 10 10:21:47 2007 +0200
+++ b/src/HOL/FunDef.thy	Thu May 10 10:21:48 2007 +0200
@@ -6,7 +6,7 @@
 header {* General recursive function definitions *}
 
 theory FunDef
-imports Accessible_Part
+imports Datatype Accessible_Part
 uses
   ("Tools/function_package/sum_tools.ML")
   ("Tools/function_package/fundef_common.ML")
isabelle