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