src/HOLCF/Ssum2.thy
changeset 2640 ee4dfce170a0
parent 1479 21eb5e156d91
child 12030 46d57d0290a2
     1.1 --- a/src/HOLCF/Ssum2.thy	Sat Feb 15 18:24:05 1997 +0100
     1.2 +++ b/src/HOLCF/Ssum2.thy	Mon Feb 17 10:57:11 1997 +0100
     1.3 @@ -8,14 +8,7 @@
     1.4  
     1.5  Ssum2 = Ssum1 + 
     1.6  
     1.7 -arities "++" :: (pcpo,pcpo)po
     1.8 -(* Witness for the above arity axiom is ssum1.ML *)
     1.9 -
    1.10 -rules
    1.11 -
    1.12 -(* instance of << for type ['a ++ 'b]  *)
    1.13 -
    1.14 -inst_ssum_po    "((op <<)::['a ++ 'b,'a ++ 'b]=>bool) = less_ssum"
    1.15 +instance "++"::(pcpo,pcpo)po (refl_less_ssum,antisym_less_ssum,trans_less_ssum)
    1.16  
    1.17  end
    1.18