--- a/src/HOL/Inductive.thy Wed May 09 07:53:04 2007 +0200
+++ b/src/HOL/Inductive.thy Wed May 09 07:53:06 2007 +0200
@@ -21,7 +21,6 @@
("Tools/datatype_case.ML")
("Tools/datatype_package.ML")
("Tools/datatype_codegen.ML")
- ("Tools/recfun_codegen.ML")
("Tools/primrec_package.ML")
begin
@@ -61,7 +60,7 @@
text {* Package setup. *}
-use "Tools/old_inductive_package.ML"
+ML {* setmp tolerate_legacy_features true use "Tools/old_inductive_package.ML" *}
setup OldInductivePackage.setup
theorems basic_monos [mono] =
@@ -90,12 +89,12 @@
then show P ..
next
assume "\<And>P\<Colon>bool. P"
- then show "False" ..
+ then show False ..
qed
lemma not_eq_False:
assumes not_eq: "x \<noteq> y"
- and eq: "x == y"
+ and eq: "x \<equiv> y"
shows False
using not_eq eq by auto
@@ -107,9 +106,6 @@
text {* Package setup. *}
-use "Tools/recfun_codegen.ML"
-setup RecfunCodegen.setup
-
use "Tools/datatype_aux.ML"
use "Tools/datatype_prop.ML"
use "Tools/datatype_rep_proofs.ML"