diff -r c5c4884634b7 -r c7af682b9ee5 src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Thu Aug 19 12:35:45 2004 +0200
+++ b/src/HOL/Recdef.thy	Fri Aug 20 12:20:09 2004 +0200
@@ -8,6 +8,8 @@
 theory Recdef
 imports Wellfounded_Relations Datatype
 files
+  ("../TFL/isand.ML")
+  ("../TFL/casesplit.ML")
   ("../TFL/utils.ML")
   ("../TFL/usyntax.ML")
   ("../TFL/dcterm.ML")
@@ -43,6 +45,8 @@
 lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
   by blast
 
+use "../TFL/isand.ML"
+use "../TFL/casesplit.ML"
 use "../TFL/utils.ML"
 use "../TFL/usyntax.ML"
 use "../TFL/dcterm.ML"