# HG changeset patch
# User wenzelm
# Date 1356819351 -3600
# Node ID 5543eff56b161bb1e9bf4529c79de7d5102065eb
# Parent  009a9fdabbad708d21c8057471d8330fce84f07e
tuned;

diff -r 009a9fdabbad -r 5543eff56b16 src/Doc/IsarRef/Inner_Syntax.thy
--- a/src/Doc/IsarRef/Inner_Syntax.thy	Sat Dec 29 17:18:01 2012 +0100
+++ b/src/Doc/IsarRef/Inner_Syntax.thy	Sat Dec 29 23:15:51 2012 +0100
@@ -353,7 +353,7 @@
   Isabelle types and terms.  Locally fixed parameters in toplevel
   theorem statements, locale and class specifications also admit
   mixfix annotations in a fairly uniform manner.  A mixfix annotation
-  describes describes the concrete syntax, the translation to abstract
+  describes the concrete syntax, the translation to abstract
   syntax, and the pretty printing.  Special case annotations provide a
   simple means of specifying infix operators and binders.