src/HOL/Complete_Partial_Order.thy
2016-01-07 wenzelm 2016-01-07 more uniform treatment of package internals;
2015-11-16 Andreas Lochbihler 2015-11-16 export internal definition
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-04-14 Andreas Lochbihler 2015-04-14 move some lemmas from AFP/Coinductive
2015-04-14 Andreas Lochbihler 2015-04-14 add lemmas
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
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