diff -r 50608ca5785c -r ad7113530c32 src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Thu Jan 11 21:51:14 2001 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Fri Jan 12 09:32:53 2001 +0100
@@ -217,11 +217,12 @@
 *}
 
 syntax
-  "_quote"       :: "'b => ('a => 'b)"                  ("(.'(_').)" [0] 1000)
-  "_antiquote"   :: "('a => 'b) => 'b"                  ("\<acute>_" [1000] 1000)
-  "_Subst"       :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"  ("_[_'/\<acute>_]" [1000] 999)
-  "_Assert"      :: "'a => 'a set"                      ("(.{_}.)" [0] 1000)
-  "_Assign"      :: "idt => 'b => 'a com"               ("(\<acute>_ :=/ _)" [70, 65] 61)
+  "_quote"       :: "'b => ('a => 'b)"       ("(.'(_').)" [0] 1000)
+  "_antiquote"   :: "('a => 'b) => 'b"       ("\<acute>_" [1000] 1000)
+  "_Subst"       :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"
+        ("_[_'/\<acute>_]" [1000] 999)
+  "_Assert"      :: "'a => 'a set"           ("(.{_}.)" [0] 1000)
+  "_Assign"      :: "idt => 'b => 'a com"    ("(\<acute>_ :=/ _)" [70, 65] 61)
   "_Cond"        :: "'a bexp => 'a com => 'a com => 'a com"
         ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
   "_While_inv"   :: "'a bexp => 'a assn => 'a com => 'a com"