# HG changeset patch
# User wenzelm
# Date 1554409112 -7200
# Node ID 43acf9a457f0be44dfd9c9a2319821ade44d3e74
# Parent  0403b5127da17a4315ce07b3940ecf169cd3cafb
tuned;

diff -r 0403b5127da1 -r 43acf9a457f0 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Thu Apr 04 22:18:16 2019 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Thu Apr 04 22:18:32 2019 +0200
@@ -665,7 +665,7 @@
     ;
 
     definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline>
-      @{syntax mixfix}? @'=' @{syntax term} + @'and');
+      @{syntax mixfix}? '=' @{syntax term} + @'and');
   \<close>
 
   The core of each interpretation command is a locale expression \<open>expr\<close>; the
@@ -1287,7 +1287,6 @@
 \<close>
 
 
-
 section \<open>Primitive specification elements\<close>
 
 subsection \<open>Sorts\<close>