--- a/src/HOLCF/ex/Hoare.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/ex/Hoare.thy Sun Oct 21 16:27:42 2007 +0200
@@ -24,9 +24,9 @@
imports HOLCF
begin
-consts
- b1 :: "'a -> tr"
- b2 :: "'a -> tr"
+axiomatization
+ b1 :: "'a -> tr" and
+ b2 :: "'a -> tr" and
g :: "'a -> 'a"
definition