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/Inductive.thy
changeset 25557 ea6b11021e79
parent 25534 d0b74fdd6067
child 26013 8764a1f1253b 
--- a/src/HOL/Inductive.thy	Thu Dec 06 12:58:01 2007 +0100
+++ b/src/HOL/Inductive.thy	Thu Dec 06 15:10:09 2007 +0100
@@ -17,6 +17,7 @@
   ("Tools/datatype_abs_proofs.ML")
   ("Tools/datatype_case.ML")
   ("Tools/datatype_package.ML")
+  ("Tools/old_primrec_package.ML")
   ("Tools/primrec_package.ML")
   ("Tools/datatype_codegen.ML")
 begin
@@ -328,6 +329,7 @@
 use "Tools/datatype_case.ML"
 use "Tools/datatype_package.ML"
 setup DatatypePackage.setup
+use "Tools/old_primrec_package.ML"
 use "Tools/primrec_package.ML"
 
 use "Tools/datatype_codegen.ML"
isabelle