removed True_implies (cf. True_implies_equals);
added header;

--- a/src/HOL/FunDef.thy	Thu Aug 03 15:03:10 2006 +0200
+++ b/src/HOL/FunDef.thy	Thu Aug 03 15:03:11 2006 +0200
@@ -1,3 +1,10 @@
+(*  Title:      HOL/FunDef.thy
+    ID:         $Id$
+    Author:     Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions. 
+*)
+
 theory FunDef
 imports Accessible_Part Datatype Recdef
 uses 
@@ -35,9 +42,6 @@
   apply (auto simp:ex1 f_def the1_equality)
   by (rule theI', rule ex1)
 
-lemma True_implies: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
-  by simp
-
 
 subsection {* Projections *}
 consts