src/HOL/Recdef.thy
changeset 23150 073a65f0bc40
parent 22622 25693088396b
child 23742 d6349ac8b153
     1.1 --- a/src/HOL/Recdef.thy	Thu May 31 13:18:42 2007 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Thu May 31 13:18:52 2007 +0200
     1.3 @@ -8,15 +8,15 @@
     1.4  theory Recdef
     1.5  imports Wellfounded_Relations FunDef
     1.6  uses
     1.7 -  ("../TFL/casesplit.ML")
     1.8 -  ("../TFL/utils.ML")
     1.9 -  ("../TFL/usyntax.ML")
    1.10 -  ("../TFL/dcterm.ML")
    1.11 -  ("../TFL/thms.ML")
    1.12 -  ("../TFL/rules.ML")
    1.13 -  ("../TFL/thry.ML")
    1.14 -  ("../TFL/tfl.ML")
    1.15 -  ("../TFL/post.ML")
    1.16 +  ("Tools/TFL/casesplit.ML")
    1.17 +  ("Tools/TFL/utils.ML")
    1.18 +  ("Tools/TFL/usyntax.ML")
    1.19 +  ("Tools/TFL/dcterm.ML")
    1.20 +  ("Tools/TFL/thms.ML")
    1.21 +  ("Tools/TFL/rules.ML")
    1.22 +  ("Tools/TFL/thry.ML")
    1.23 +  ("Tools/TFL/tfl.ML")
    1.24 +  ("Tools/TFL/post.ML")
    1.25    ("Tools/recdef_package.ML")
    1.26  begin
    1.27  
    1.28 @@ -44,15 +44,15 @@
    1.29  lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
    1.30    by blast
    1.31  
    1.32 -use "../TFL/casesplit.ML"
    1.33 -use "../TFL/utils.ML"
    1.34 -use "../TFL/usyntax.ML"
    1.35 -use "../TFL/dcterm.ML"
    1.36 -use "../TFL/thms.ML"
    1.37 -use "../TFL/rules.ML"
    1.38 -use "../TFL/thry.ML"
    1.39 -use "../TFL/tfl.ML"
    1.40 -use "../TFL/post.ML"
    1.41 +use "Tools/TFL/casesplit.ML"
    1.42 +use "Tools/TFL/utils.ML"
    1.43 +use "Tools/TFL/usyntax.ML"
    1.44 +use "Tools/TFL/dcterm.ML"
    1.45 +use "Tools/TFL/thms.ML"
    1.46 +use "Tools/TFL/rules.ML"
    1.47 +use "Tools/TFL/thry.ML"
    1.48 +use "Tools/TFL/tfl.ML"
    1.49 +use "Tools/TFL/post.ML"
    1.50  use "Tools/recdef_package.ML"
    1.51  setup RecdefPackage.setup
    1.52  
    1.53 @@ -63,7 +63,7 @@
    1.54    same_fst_def
    1.55    less_Suc_eq [THEN iffD2]
    1.56  
    1.57 -lemmas [recdef_cong] = 
    1.58 +lemmas [recdef_cong] =
    1.59    if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
    1.60  
    1.61  lemmas [recdef_wf] =