src/HOL/Hoare/Hoare.thy

--- a/src/HOL/Hoare/Hoare.thy	Thu Nov 28 15:44:34 2002 +0100
+++ b/src/HOL/Hoare/Hoare.thy	Fri Nov 29 09:48:28 2002 +0100
@@ -57,10 +57,10 @@
 
 syntax
  "@hoare_vars" :: "[vars, 'a assn,'a com,'a assn] => bool"
-                 ("|- VARS _.// {_} // _ // {_}" [0,0,55,0] 50)
+                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
 syntax ("" output)
  "@hoare"      :: "['a assn,'a com,'a assn] => bool"
-                 ("|- {_} // _ // {_}" [0,55,0] 50)
+                 ("{_} // _ // {_}" [0,55,0] 50)
 
 (** parse translations **)