--- a/src/HOL/Library/Old_Recdef.thy Fri Jun 19 18:41:21 2015 +0200
+++ b/src/HOL/Library/Old_Recdef.thy Fri Jun 19 19:13:15 2015 +0200
@@ -14,7 +14,7 @@
subsection \<open>Lemmas for TFL\<close>
-lemma tfl_wf_induct: "ALL R. wf R -->
+lemma tfl_wf_induct: "ALL R. wf R -->
(ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
apply clarify
apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
@@ -58,16 +58,7 @@
lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
by blast
-ML_file "~~/src/HOL/Tools/TFL/casesplit.ML"
-ML_file "~~/src/HOL/Tools/TFL/utils.ML"
-ML_file "~~/src/HOL/Tools/TFL/usyntax.ML"
-ML_file "~~/src/HOL/Tools/TFL/dcterm.ML"
-ML_file "~~/src/HOL/Tools/TFL/thms.ML"
-ML_file "~~/src/HOL/Tools/TFL/rules.ML"
-ML_file "~~/src/HOL/Tools/TFL/thry.ML"
-ML_file "~~/src/HOL/Tools/TFL/tfl.ML"
-ML_file "~~/src/HOL/Tools/TFL/post.ML"
-ML_file "~~/src/HOL/Tools/recdef.ML"
+ML_file "old_recdef.ML"
subsection \<open>Rule setup\<close>
@@ -81,7 +72,7 @@
lemmas [recdef_cong] =
if_cong let_cong image_cong INF_cong SUP_cong bex_cong ball_cong imp_cong
- map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong
+ map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong
lemmas [recdef_wf] =
wf_trancl