author | wenzelm |
Fri, 09 Nov 2001 00:20:26 +0100 | |
changeset 12124 | c4fcdb80c93e |
parent 12123 | 739eba13e2cd |
child 12125 | 316d11f760f7 |
--- 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)