src/HOL/Complete_Partial_Order.thy
2013-12-05 Andreas Lochbihler 2013-12-05 restrict admissibility to non-empty chains to allow more syntax-directed proof rules
2013-09-02 Andreas Lochbihler 2013-09-02 move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
2011-12-29 huffman 2011-12-29 remove constant 'ccpo.lub', re-use constant 'Sup' instead
2010-10-29 krauss 2010-10-29 hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
2010-10-23 krauss 2010-10-23 Complete_Partial_Order.thy: complete partial orders over arbitrary chains, with fixpoint theorem