src/HOL/Isar_examples/Hoare.thy
changeset 12124 c4fcdb80c93e
parent 11987 bf31b35949ce
child 13703 a36a0d417133
--- a/src/HOL/Isar_examples/Hoare.thy	Fri Nov 09 00:19:20 2001 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Fri Nov 09 00:20:26 2001 +0100
@@ -60,7 +60,7 @@
     ("(3|- _/ (2_)/ _)" [100, 55, 100] 50)
   "|- P c Q == ALL s s'. Sem c s s' --> s : P --> s' : Q"
 
-syntax (symbols)
+syntax (xsymbols)
   Valid :: "'a bexp => 'a com => 'a bexp => bool"
     ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)