equal
deleted
inserted
replaced
7 define constants for categorical reasoning |
7 define constants for categorical reasoning |
8 *) |
8 *) |
9 |
9 |
10 ccc1 = Cprod3 + Sprod3 + Ssum3 + Up3 + Fix + |
10 ccc1 = Cprod3 + Sprod3 + Ssum3 + Up3 + Fix + |
11 |
11 |
12 instance flat<chfin (flat_subclass_chfin) |
12 instance flat<chfin (flat_imp_chain_finite) |
13 |
13 |
14 consts |
14 consts |
15 ID :: "('a::cpo) -> 'a" |
15 ID :: "('a::cpo) -> 'a" |
16 cfcomp :: "('b->'c)->(('a::cpo)->('b::cpo))->'a->('c::cpo)" |
16 cfcomp :: "('b->'c)->(('a::cpo)->('b::cpo))->'a->('c::cpo)" |
17 |
17 |