src/HOL/Library/Old_Recdef.thy
changeset 60520 09fc5eaa21ce
parent 60500 903bb1495239
child 60523 be2d9f5ddc76
     1.1 --- a/src/HOL/Library/Old_Recdef.thy	Fri Jun 19 18:41:21 2015 +0200
     1.2 +++ b/src/HOL/Library/Old_Recdef.thy	Fri Jun 19 19:13:15 2015 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  subsection \<open>Lemmas for TFL\<close>
     1.6  
     1.7 -lemma tfl_wf_induct: "ALL R. wf R -->  
     1.8 +lemma tfl_wf_induct: "ALL R. wf R -->
     1.9         (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
    1.10  apply clarify
    1.11  apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
    1.12 @@ -58,16 +58,7 @@
    1.13  lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
    1.14    by blast
    1.15  
    1.16 -ML_file "~~/src/HOL/Tools/TFL/casesplit.ML"
    1.17 -ML_file "~~/src/HOL/Tools/TFL/utils.ML"
    1.18 -ML_file "~~/src/HOL/Tools/TFL/usyntax.ML"
    1.19 -ML_file "~~/src/HOL/Tools/TFL/dcterm.ML"
    1.20 -ML_file "~~/src/HOL/Tools/TFL/thms.ML"
    1.21 -ML_file "~~/src/HOL/Tools/TFL/rules.ML"
    1.22 -ML_file "~~/src/HOL/Tools/TFL/thry.ML"
    1.23 -ML_file "~~/src/HOL/Tools/TFL/tfl.ML"
    1.24 -ML_file "~~/src/HOL/Tools/TFL/post.ML"
    1.25 -ML_file "~~/src/HOL/Tools/recdef.ML"
    1.26 +ML_file "old_recdef.ML"
    1.27  
    1.28  
    1.29  subsection \<open>Rule setup\<close>
    1.30 @@ -81,7 +72,7 @@
    1.31  
    1.32  lemmas [recdef_cong] =
    1.33    if_cong let_cong image_cong INF_cong SUP_cong bex_cong ball_cong imp_cong
    1.34 -  map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong 
    1.35 +  map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong
    1.36  
    1.37  lemmas [recdef_wf] =
    1.38    wf_trancl