--- a/src/HOL/Isar_Examples/Hoare.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Wed Feb 24 22:09:50 2010 +0100
@@ -60,9 +60,8 @@
("(3|- _/ (2_)/ _)" [100, 55, 100] 50)
"|- P c Q == ALL s s'. Sem c s s' --> s : P --> s' : Q"
-syntax (xsymbols)
- Valid :: "'a bexp => 'a com => 'a bexp => bool"
- ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
+notation (xsymbols)
+ Valid ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
lemma ValidI [intro?]:
"(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q"