Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hoare/Hoare_Logic.thy
changeset 35416 d8d7d1b785af
parent 35316 870dfea4f9c0
child 36643 f36588af1ba1 
--- a/src/HOL/Hoare/Hoare_Logic.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -40,7 +40,7 @@
                                       (s ~: b --> Sem c2 s s'))"
 "Sem(While b x c) s s' = (? n. iter n b (Sem c) s s')"
 
-constdefs Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
   "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
isabelle