--- 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}.
*}
--- 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}}
+