equal
deleted
inserted
replaced
6 introduction of the classes cpo and pcpo |
6 introduction of the classes cpo and pcpo |
7 *) |
7 *) |
8 |
8 |
9 header {* Classes cpo and pcpo *} |
9 header {* Classes cpo and pcpo *} |
10 |
10 |
11 theory Pcpo = Porder: |
11 theory Pcpo |
|
12 imports Porder |
|
13 begin |
12 |
14 |
13 (* The class cpo of chain complete partial orders *) |
15 (* The class cpo of chain complete partial orders *) |
14 (* ********************************************** *) |
16 (* ********************************************** *) |
15 axclass cpo < po |
17 axclass cpo < po |
16 (* class axiom: *) |
18 (* class axiom: *) |