diff -r 1810b1ade437 -r 47ee18b6ae32 src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Mon Mar 01 12:30:55 2010 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Mon Mar 01 13:42:31 2010 +0100
@@ -55,13 +55,10 @@
     (if s : b then Sem c1 s s' else Sem c2 s s')"
   "Sem (While b x c) s s' = (EX n. iter n b (Sem c) s s')"
 
-constdefs
-  Valid :: "'a bexp => 'a com => 'a bexp => bool"
-    ("(3|- _/ (2_)/ _)" [100, 55, 100] 50)
+definition Valid :: "'a bexp => 'a com => 'a bexp => bool" ("(3|- _/ (2_)/ _)" [100, 55, 100] 50) where
   "|- P c Q == ALL s s'. Sem c s s' --> s : P --> s' : Q"
 
-notation (xsymbols)
-  Valid  ("(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"