equal
deleted
inserted
replaced
217 demanding keyword 'by' and supporting the full method expression |
217 demanding keyword 'by' and supporting the full method expression |
218 syntax just like the Isar command 'by'. |
218 syntax just like the Isar command 'by'. |
219 |
219 |
220 |
220 |
221 *** HOL *** |
221 *** HOL *** |
|
222 |
|
223 * Theory Library/Diagonalize.thy provides constructive version of |
|
224 Cantor's first diagonalization argument. |
222 |
225 |
223 * New predicate "strict_mono" classifies strict functions on partial orders. |
226 * New predicate "strict_mono" classifies strict functions on partial orders. |
224 With strict functions on linear orders, reasoning about (in)equalities is |
227 With strict functions on linear orders, reasoning about (in)equalities is |
225 facilitated by theorems "strict_mono_eq", "strict_mono_less_eq" and "strict_mono_less". |
228 facilitated by theorems "strict_mono_eq", "strict_mono_less_eq" and "strict_mono_less". |
226 |
229 |