shifted "fun" command to Wellfounded_Relations
authorhaftmann
Mon Dec 03 16:04:14 2007 +0100 (2007-12-03)
changeset 2551736d710d1dbce
parent 25516 ad25835675b9
child 25518 00d5cc16e891
shifted "fun" command to Wellfounded_Relations
src/HOL/PreList.thy
src/HOL/Wellfounded_Relations.thy
     1.1 --- a/src/HOL/PreList.thy	Mon Dec 03 16:04:13 2007 +0100
     1.2 +++ b/src/HOL/PreList.thy	Mon Dec 03 16:04:14 2007 +0100
     1.3 @@ -8,8 +8,6 @@
     1.4  
     1.5  theory PreList
     1.6  imports ATP_Linkup
     1.7 -uses "Tools/function_package/lexicographic_order.ML"
     1.8 -     "Tools/function_package/fundef_datatype.ML"
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -17,8 +15,4 @@
    1.13    theory ToyList in the documentation.
    1.14  *}
    1.15  
    1.16 -(* The lexicographic_order method and the "fun" command *)
    1.17 -setup LexicographicOrder.setup
    1.18 -setup FundefDatatype.setup
    1.19 -
    1.20  end
     2.1 --- a/src/HOL/Wellfounded_Relations.thy	Mon Dec 03 16:04:13 2007 +0100
     2.2 +++ b/src/HOL/Wellfounded_Relations.thy	Mon Dec 03 16:04:14 2007 +0100
     2.3 @@ -6,7 +6,10 @@
     2.4  header {*Well-founded Relations*}
     2.5  
     2.6  theory Wellfounded_Relations
     2.7 -imports Finite_Set
     2.8 +imports Finite_Set FunDef
     2.9 +uses
    2.10 +  ("Tools/function_package/lexicographic_order.ML")
    2.11 +  ("Tools/function_package/fundef_datatype.ML")
    2.12  begin
    2.13  
    2.14  text{*Derived WF relations such as inverse image, lexicographic product and
    2.15 @@ -266,4 +269,15 @@
    2.16  apply (intro wf_trancl wf_pred_nat)
    2.17  done
    2.18  
    2.19 +
    2.20 +text {*
    2.21 +  Setup of @{text lexicographic_order} method
    2.22 +  and @{text fun} command
    2.23 +*}
    2.24 +
    2.25 +use "Tools/function_package/lexicographic_order.ML"
    2.26 +use "Tools/function_package/fundef_datatype.ML"
    2.27 +
    2.28 +setup "LexicographicOrder.setup #> FundefDatatype.setup"
    2.29 +
    2.30  end