equal
deleted
inserted
replaced
77 Conditionally_Complete_Lattices. INCOMPATIBILITY. |
77 Conditionally_Complete_Lattices. INCOMPATIBILITY. |
78 |
78 |
79 * Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them |
79 * Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them |
80 instead of explicitly stating boundedness of sets. |
80 instead of explicitly stating boundedness of sets. |
81 |
81 |
|
82 * ccpo.admissible quantifies only over non-empty chains to allow |
|
83 more syntax-directed proof rules; the case of the empty chain |
|
84 shows up as additional case in fixpoint induction proofs. |
|
85 INCOMPATIBILITY |
82 |
86 |
83 *** ML *** |
87 *** ML *** |
84 |
88 |
85 * Toplevel function "use" refers to raw ML bootstrap environment, |
89 * Toplevel function "use" refers to raw ML bootstrap environment, |
86 without Isar context nor antiquotations. Potential INCOMPATIBILITY. |
90 without Isar context nor antiquotations. Potential INCOMPATIBILITY. |