src/HOLCF/ex/Hoare.thy
changeset 2380 90280b3a538b
parent 2379 2e55b396e24c
child 10835 f4745d77e620
equal deleted inserted replaced
2379:2e55b396e24c 2380:90280b3a538b
    19 In order to get a nice notation we fix the functions b1,b2 and g in the
    19 In order to get a nice notation we fix the functions b1,b2 and g in the
    20 signature of this example
    20 signature of this example
    21 
    21 
    22 *)
    22 *)
    23 
    23 
    24 Hoare = HOLCF +
    24 Hoare = HOLCF + 
    25 
    25 
    26 consts
    26 consts
    27         b1:: "'a -> tr"
    27         b1:: "'a -> tr"
    28         b2:: "'a -> tr"
    28         b2:: "'a -> tr"
    29          g:: "'a -> 'a"
    29          g:: "'a -> 'a"