src/Doc/Logics_ZF/ZF_Isar.thy
changeset 58620 7435b6a3f72e
parent 56451 856492b0f755
child 62969 9f394a16c557
--- a/src/Doc/Logics_ZF/ZF_Isar.thy	Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Logics_ZF/ZF_Isar.thy	Tue Oct 07 22:35:11 2014 +0200
@@ -94,7 +94,7 @@
     hints: @{syntax (ZF) "monos"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
   \<close>}
 
-  See \cite{isabelle-ZF} for further information on inductive
+  See @{cite "isabelle-ZF"} for further information on inductive
   definitions in ZF, but note that this covers the old-style theory
   format.
 *}