# HG changeset patch
# User wenzelm
# Date 1412845215 -7200
# Node ID 5855b9b3d6a3d0712587f8aeb062bb3351210e01
# Parent  9b33fe5b60f3084105bb4ca63c069e12a60b9364
proper @{cite} with bibtex entry (unchecked comment);

diff -r 9b33fe5b60f3 -r 5855b9b3d6a3 src/ZF/Induct/Primrec.thy
--- a/src/ZF/Induct/Primrec.thy	Wed Oct 08 18:10:17 2014 +0200
+++ b/src/ZF/Induct/Primrec.thy	Thu Oct 09 11:00:15 2014 +0200
@@ -10,7 +10,7 @@
 text {*
   Proof adopted from @{cite szasz93}.
 
-  See also \cite[page 250, exercise 11]{mendelson}.
+  See also @{cite \<open>page 250, exercise 11\<close> mendelson}.
 *}
 
 
diff -r 9b33fe5b60f3 -r 5855b9b3d6a3 src/ZF/Induct/document/root.bib
--- a/src/ZF/Induct/document/root.bib	Wed Oct 08 18:10:17 2014 +0200
+++ b/src/ZF/Induct/document/root.bib	Thu Oct 09 11:00:15 2014 +0200
@@ -27,3 +27,10 @@
   publisher	= CUP,
   year		= 1993}
 
+@book{mendelson,
+  Author = {E. Mendelson},
+  Edition = {Fourth},
+  Publisher = {Chapman \& Hall},
+  Title = {Introduction to Mathematical Logic},
+  Year = {1997}}
+