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/HOLCF/IMP/HoareEx.thy
changeset 80914 d97fdabd9e2b
parent 76987 4c275405faae 
--- a/src/HOL/HOLCF/IMP/HoareEx.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -16,7 +16,7 @@
 type_synonym assn = "state \<Rightarrow> bool"
 
 definition
-  hoare_valid :: "[assn, com, assn] \<Rightarrow> bool"  ("|= {(1_)}/ (_)/ {(1_)}" 50) where
+  hoare_valid :: "[assn, com, assn] \<Rightarrow> bool"  (\<open>|= {(1_)}/ (_)/ {(1_)}\<close> 50) where
   "|= {P} c {Q} = (\<forall>s t. P s \<and> D c\<cdot>(Discr s) = Def t \<longrightarrow> Q t)"
 
 lemma WHILE_rule_sound:
isabelle