| 2015-04-14 | Andreas Lochbihler | 2015-04-14 | move some lemmas from AFP/Coinductive | file | diff | annotate |
| 2015-04-14 | Andreas Lochbihler | 2015-04-14 | add lemmas | file | diff | annotate |
| 2014-11-02 | wenzelm | 2014-11-02 | modernized header uniformly as section; | file | diff | annotate |
| 2013-12-05 | Andreas Lochbihler | 2013-12-05 | restrict admissibility to non-empty chains to allow more syntax-directed proof rules | file | diff | annotate |
| 2013-09-02 | Andreas Lochbihler | 2013-09-02 | move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems | file | diff | annotate |
| 2011-12-29 | huffman | 2011-12-29 | remove constant 'ccpo.lub', re-use constant 'Sup' instead | file | diff | annotate |
| 2010-10-29 | krauss | 2010-10-29 | hide_const various constants, in particular to avoid ugly qualifiers in HOLCF | file | diff | annotate |
| 2010-10-23 | krauss | 2010-10-23 | Complete_Partial_Order.thy: complete partial orders over arbitrary chains, with fixpoint theorem | file | diff | annotate |