src/HOL/Recdef.thy
changeset 15481 fc075ae929e4
parent 15150 c7af682b9ee5
child 16417 9bc16273c2d4
--- a/src/HOL/Recdef.thy	Sun Jan 30 20:48:50 2005 +0100
+++ b/src/HOL/Recdef.thy	Tue Feb 01 18:01:57 2005 +0100
@@ -8,7 +8,6 @@
 theory Recdef
 imports Wellfounded_Relations Datatype
 files
-  ("../TFL/isand.ML")
   ("../TFL/casesplit.ML")
   ("../TFL/utils.ML")
   ("../TFL/usyntax.ML")
@@ -45,7 +44,6 @@
 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"