# HG changeset patch
# User haftmann
# Date 1196694254 -3600
# Node ID 36d710d1dbcedad91c874dea42ee62c2f93f9949
# Parent  ad25835675b9a3be2da94e565b2e052877eb5cfc
shifted "fun" command to Wellfounded_Relations

diff -r ad25835675b9 -r 36d710d1dbce src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Mon Dec 03 16:04:13 2007 +0100
+++ b/src/HOL/PreList.thy	Mon Dec 03 16:04:14 2007 +0100
@@ -8,8 +8,6 @@
 
 theory PreList
 imports ATP_Linkup
-uses "Tools/function_package/lexicographic_order.ML"
-     "Tools/function_package/fundef_datatype.ML"
 begin
 
 text {*
@@ -17,8 +15,4 @@
   theory ToyList in the documentation.
 *}
 
-(* The lexicographic_order method and the "fun" command *)
-setup LexicographicOrder.setup
-setup FundefDatatype.setup
-
 end
diff -r ad25835675b9 -r 36d710d1dbce src/HOL/Wellfounded_Relations.thy
--- a/src/HOL/Wellfounded_Relations.thy	Mon Dec 03 16:04:13 2007 +0100
+++ b/src/HOL/Wellfounded_Relations.thy	Mon Dec 03 16:04:14 2007 +0100
@@ -6,7 +6,10 @@
 header {*Well-founded Relations*}
 
 theory Wellfounded_Relations
-imports Finite_Set
+imports Finite_Set FunDef
+uses
+  ("Tools/function_package/lexicographic_order.ML")
+  ("Tools/function_package/fundef_datatype.ML")
 begin
 
 text{*Derived WF relations such as inverse image, lexicographic product and
@@ -266,4 +269,15 @@
 apply (intro wf_trancl wf_pred_nat)
 done
 
+
+text {*
+  Setup of @{text lexicographic_order} method
+  and @{text fun} command
+*}
+
+use "Tools/function_package/lexicographic_order.ML"
+use "Tools/function_package/fundef_datatype.ML"
+
+setup "LexicographicOrder.setup #> FundefDatatype.setup"
+
 end