| changeset 55381 | ca31f042414f |
| parent 51717 | 9e7d1c139569 |
| child 62175 | 8ffc4d0e652d |
--- a/src/HOL/HOLCF/ex/Focus_ex.thy Mon Feb 10 17:20:11 2014 +0100 +++ b/src/HOL/HOLCF/ex/Focus_ex.thy Mon Feb 10 17:23:13 2014 +0100 @@ -103,7 +103,8 @@ begin typedecl ('a, 'b) tc -arities tc:: (pcpo, pcpo) pcpo +axiomatization where tc_arity: "OFCLASS(('a::pcpo, 'b::pcpo) tc, pcop_class)" +instance tc :: (pcpo, pcpo) pcpo by (rule tc_arity) axiomatization Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"