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)