# HG changeset patch
# User wenzelm
# Date 1154610191 -7200
# Node ID 71d63a30cc964b0a478e6deb4ba70aef6ceaccef
# Parent  ac413d7cc03d82d20e0d87b658e61a7fd5a5bdc7
removed True_implies (cf. True_implies_equals);
added header;

diff -r ac413d7cc03d -r 71d63a30cc96 src/HOL/FunDef.thy
--- 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