--- 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"