# 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