--- a/src/HOL/FunDef.thy Thu Jun 19 00:02:08 2008 +0200
+++ b/src/HOL/FunDef.thy Thu Jun 19 11:46:14 2008 +0200
@@ -18,10 +18,10 @@
("Tools/function_package/pattern_split.ML")
("Tools/function_package/fundef_package.ML")
("Tools/function_package/auto_term.ML")
- ("Tools/function_package/induction_scheme.ML")
("Tools/function_package/measure_functions.ML")
("Tools/function_package/lexicographic_order.ML")
("Tools/function_package/fundef_datatype.ML")
+ ("Tools/function_package/induction_scheme.ML")
begin
text {* Definitions with default value. *}
@@ -110,10 +110,10 @@
use "Tools/function_package/pattern_split.ML"
use "Tools/function_package/auto_term.ML"
use "Tools/function_package/fundef_package.ML"
-use "Tools/function_package/induction_scheme.ML"
use "Tools/function_package/measure_functions.ML"
use "Tools/function_package/lexicographic_order.ML"
use "Tools/function_package/fundef_datatype.ML"
+use "Tools/function_package/induction_scheme.ML"
setup {*
FundefPackage.setup