--- 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"