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"