--- 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>