# HG changeset patch
# User wenzelm
# Date 1148752147 -7200
# Node ID 3b8920131be24f4b7d64a51f87bcae4a4db13aab
# Parent  d8d0f8f51d69d36188ec45ff68bee1fc377e45fa
tuned;

diff -r d8d0f8f51d69 -r 3b8920131be2 src/HOLCF/IMP/Denotational.thy
--- 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"
 
diff -r d8d0f8f51d69 -r 3b8920131be2 src/HOLCF/IMP/HoareEx.thy
--- 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}"