| changeset 12338 | de0f4a63baa5 |
| parent 12030 | 46d57d0290a2 |
| child 14981 | e73f8140af78 |
| 12337:7c6a970f0808 | 12338:de0f4a63baa5 |
|---|---|
11 Fun1 = Pcpo + |
11 Fun1 = Pcpo + |
12 |
12 |
13 instance flat<chfin (flat_imp_chfin) |
13 instance flat<chfin (flat_imp_chfin) |
14 |
14 |
15 (* to make << defineable: *) |
15 (* to make << defineable: *) |
16 instance fun :: (term,sq_ord)sq_ord |
16 instance fun :: (type, sq_ord) sq_ord |
17 |
17 |
18 defs |
18 defs |
19 less_fun_def "(op <<) == (%f1 f2.!x. f1 x << f2 x)" |
19 less_fun_def "(op <<) == (%f1 f2.!x. f1 x << f2 x)" |
20 end |
20 end |
21 |
21 |