src/HOLCF/ex/Hoare.thy
changeset 25135 4f8176c940cf
parent 21404 eb85850d3eb7
child 25895 0eaadfa8889e
     1.1 --- a/src/HOLCF/ex/Hoare.thy	Sun Oct 21 14:53:44 2007 +0200
     1.2 +++ b/src/HOLCF/ex/Hoare.thy	Sun Oct 21 16:27:42 2007 +0200
     1.3 @@ -24,9 +24,9 @@
     1.4  imports HOLCF
     1.5  begin
     1.6  
     1.7 -consts
     1.8 -  b1 :: "'a -> tr"
     1.9 -  b2 :: "'a -> tr"
    1.10 +axiomatization
    1.11 +  b1 :: "'a -> tr" and
    1.12 +  b2 :: "'a -> tr" and
    1.13    g :: "'a -> 'a"
    1.14  
    1.15  definition