# HG changeset patch
# User wenzelm
# Date 1412718754 -7200
# Node ID 75b9b64ccb584982ff58f93ffdaafd983fd0e0df
# Parent  2db1df2c84676d94a81b0ea18888ffc76ba4e7c9
more antiquotations;

diff -r 2db1df2c8467 -r 75b9b64ccb58 src/ZF/Induct/Primrec.thy
--- a/src/ZF/Induct/Primrec.thy	Tue Oct 07 23:29:43 2014 +0200
+++ b/src/ZF/Induct/Primrec.thy	Tue Oct 07 23:52:34 2014 +0200
@@ -8,7 +8,7 @@
 theory Primrec imports Main begin
 
 text {*
-  Proof adopted from \cite{szasz93}.
+  Proof adopted from @{cite szasz93}.
 
   See also \cite[page 250, exercise 11]{mendelson}.
 *}