1.1 --- a/src/HOL/Recdef.thy	Sun Jan 30 20:48:50 2005 +0100
     1.2 +++ b/src/HOL/Recdef.thy	Tue Feb 01 18:01:57 2005 +0100
     1.3 @@ -8,7 +8,6 @@
     1.4  theory Recdef
     1.5  imports Wellfounded_Relations Datatype
     1.6  files
     1.7 -  ("../TFL/isand.ML")
     1.8    ("../TFL/casesplit.ML")
     1.9    ("../TFL/utils.ML")
    1.10    ("../TFL/usyntax.ML")
    1.11 @@ -45,7 +44,6 @@
    1.12  lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
    1.13    by blast
    1.14  
    1.15 -use "../TFL/isand.ML"
    1.16  use "../TFL/casesplit.ML"
    1.17  use "../TFL/utils.ML"
    1.18  use "../TFL/usyntax.ML"