src/HOLCF/Up2.thy
changeset 2640 ee4dfce170a0
parent 2278 d63ffafce255
child 12030 46d57d0290a2
     1.1 --- a/src/HOLCF/Up2.thy	Sat Feb 15 18:24:05 1997 +0100
     1.2 +++ b/src/HOLCF/Up2.thy	Mon Feb 17 10:57:11 1997 +0100
     1.3 @@ -9,15 +9,7 @@
     1.4  
     1.5  Up2 = Up1 + 
     1.6  
     1.7 -(* Witness for the above arity axiom is up1.ML *)
     1.8 -
     1.9 -arities "u" :: (pcpo)po
    1.10 -
    1.11 -rules
    1.12 -
    1.13 -(* instance of << for type ('a)u  *)
    1.14 -
    1.15 -inst_up_po    "((op <<)::[('a)u,('a)u]=>bool) = less_up"
    1.16 +instance u :: (pcpo)po (refl_less_up,antisym_less_up,trans_less_up)
    1.17  
    1.18  end
    1.19