eliminated old "symbols" syntax, use "xsymbols" instead;
authorwenzelm
Fri, 09 Nov 2001 00:20:26 +0100
changeset 12124 c4fcdb80c93e
parent 12123 739eba13e2cd
child 12125 316d11f760f7
eliminated old "symbols" syntax, use "xsymbols" instead;
src/HOL/Isar_examples/Hoare.thy
--- 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)