diff -r d5ff8b782b29 -r fee7cfa69c50 src/Doc/Logics_ZF/ZF_examples.thy
--- a/src/Doc/Logics_ZF/ZF_examples.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Logics_ZF/ZF_examples.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -42,7 +42,7 @@
 
 text {*
 @{thm[display] Br_in_bt[no_vars]}
-*};
+*}
 
 subsection{*Primitive recursion*}
 
@@ -92,7 +92,7 @@
 
 
 consts
-  llist  :: "i=>i";
+  llist  :: "i=>i"
 
 codatatype
   "llist(A)" = LNil | LCons ("a \<in> A", "l \<in> llist(A)")