# HG changeset patch
# User haftmann
# Date 1225193397 -3600
# Node ID 4867f2fa0e48c55a17993b8cec3d2145bea7d9e6
# Parent  ca5840b1f7b3851050d034dc271cf02e07f94416
removed includes

diff -r ca5840b1f7b3 -r 4867f2fa0e48 src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Tue Oct 28 12:28:14 2008 +0100
+++ b/src/HOL/Library/Coinductive_List.thy	Tue Oct 28 12:29:57 2008 +0100
@@ -216,7 +216,7 @@
     CONS_type Abs_llist_inverse Rep_llist Rep_llist_inverse inj_Leaf)
 
 lemma llist_case_cert:
-  includes meta_conjunction_syntax
+  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   assumes "CASE \<equiv> llist_case c d"
   shows "(CASE LNil \<equiv> c) && (CASE (LCons M N) \<equiv> d M N)"
   using assms by simp_all