Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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"
isabelle