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 74723 f05c73bf5968
parent 74503 403ce50e6a2a 
--- a/src/HOL/Hoare/Hoare_Logic.thy	Sun Nov 07 10:07:09 2021 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Sun Nov 07 14:26:11 2021 +0100
@@ -134,8 +134,8 @@
   assumes "p \<subseteq> i"
       and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (A n) (i \<inter> {s . v s < n})"
       and "i \<inter> uminus b \<subseteq> q"
-    shows "ValidTC p (While b c) (Awhile i v A) q"
-proof -
+    shows "ValidTC p (While b c) (Awhile i v (\<lambda>n. A n)) q"
+proof -                             
   {
     fix s n
     have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)"
isabelle