--- a/src/HOLCF/IMP/Denotational.thy Sat May 27 17:42:02 2006 +0200
+++ b/src/HOLCF/IMP/Denotational.thy Sat May 27 19:49:07 2006 +0200
@@ -10,9 +10,9 @@
subsection "Definition"
-constdefs
+definition
dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)"
- "dlift f == (LAM x. case x of UU => UU | Def y => f\<cdot>(Discr y))"
+ "dlift f = (LAM x. case x of UU => UU | Def y => f\<cdot>(Discr y))"
consts D :: "com => state discr -> state lift"
--- a/src/HOLCF/IMP/HoareEx.thy Sat May 27 17:42:02 2006 +0200
+++ b/src/HOLCF/IMP/HoareEx.thy Sat May 27 19:49:07 2006 +0200
@@ -16,9 +16,9 @@
types assn = "state => bool"
-constdefs
+definition
hoare_valid :: "[assn, com, assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50)
- "|= {A} c {B} == \<forall>s t. A s \<and> D c $(Discr s) = Def t --> B t"
+ "|= {A} c {B} = (\<forall>s t. A s \<and> D c $(Discr s) = Def t --> B t)"
lemma WHILE_rule_sound:
"|= {A} c {A} ==> |= {A} \<WHILE> b \<DO> c {\<lambda>s. A s \<and> \<not> b s}"