# HG changeset patch
# User wenzelm
# Date 1005261626 -3600
# Node ID c4fcdb80c93e29813f9c0600c074203ad766a541
# Parent  739eba13e2cddd9c7d63fa581933b682f04de450
eliminated old "symbols" syntax, use "xsymbols" instead;

diff -r 739eba13e2cd -r c4fcdb80c93e 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)