src/Doc/Tutorial/Types/Records.thy
changeset 58620 7435b6a3f72e
parent 48985 5386df44a037
child 58889 5b7a9633cfa8
--- a/src/Doc/Tutorial/Types/Records.thy	Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/Types/Records.thy	Tue Oct 07 22:35:11 2014 +0200
@@ -33,7 +33,7 @@
 
 text {*
   Record types are not primitive in Isabelle and have a delicate
-  internal representation \cite{NaraschewskiW-TPHOLs98}, based on
+  internal representation @{cite "NaraschewskiW-TPHOLs98"}, based on
   nested copies of the primitive product type.  A \commdx{record}
   declaration introduces a new record type scheme by specifying its
   fields, which are packaged internally to hold up the perception of