src/HOL/Recdef.thy
changeset 11454 7514e5e21cb8
parent 11284 981ea92a86dd
child 11533 0c0d2332e8f0
     1.1 --- a/src/HOL/Recdef.thy	Wed Jul 25 13:44:32 2001 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Wed Jul 25 17:58:26 2001 +0200
     1.3 @@ -17,9 +17,6 @@
     1.4    ("../TFL/post.ML")
     1.5    ("Tools/recdef_package.ML"):
     1.6  
     1.7 -lemma tfl_some: "\\<forall>P x. P x --> P (Eps P)"
     1.8 -  by (blast intro: someI)
     1.9 -
    1.10  lemma tfl_eq_True: "(x = True) --> x"
    1.11    by blast
    1.12