Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/FunDef.thy
changeset 23494 f985f9239e0d
parent 23203 a5026e73cfcf
child 23739 c5ead5df7f35 
--- a/src/HOL/FunDef.thy	Mon Jun 25 00:36:42 2007 +0200
+++ b/src/HOL/FunDef.thy	Mon Jun 25 12:16:27 2007 +0200
@@ -8,7 +8,6 @@
 theory FunDef
 imports Datatype Accessible_Part
 uses
-  ("Tools/function_package/sum_tools.ML")
   ("Tools/function_package/fundef_lib.ML")
   ("Tools/function_package/fundef_common.ML")
   ("Tools/function_package/inductive_wrap.ML")
@@ -86,8 +85,6 @@
     by (rule THE_default_none)
 qed
 
-
-use "Tools/function_package/sum_tools.ML"
 use "Tools/function_package/fundef_lib.ML"
 use "Tools/function_package/fundef_common.ML"
 use "Tools/function_package/inductive_wrap.ML"
isabelle