src/HOL/Induct/LList.thy

--- a/src/HOL/Induct/LList.thy	Wed Dec 15 10:19:19 2004 +0100
+++ b/src/HOL/Induct/LList.thy	Wed Dec 15 17:32:40 2004 +0100
@@ -443,12 +443,6 @@
 
 subsection{* Isomorphisms *}
 
-lemma inj_Rep_LList: "inj Rep_LList"
-apply (rule inj_on_inverseI)
-apply (rule Rep_LList_inverse)
-done
-
-
 lemma LListI: "x \<in> llist (range Leaf) ==> x \<in> LList"
 by (unfold LList_def, simp)