src/HOL/Complete_Partial_Order.thy
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Tue, 14 Apr 2015 13:56:34 +0200 Andreas Lochbihler move some lemmas from AFP/Coinductive
Tue, 14 Apr 2015 11:32:01 +0200 Andreas Lochbihler add lemmas
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 05 Dec 2013 09:20:32 +0100 Andreas Lochbihler restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Mon, 02 Sep 2013 16:28:11 +0200 Andreas Lochbihler move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
Thu, 29 Dec 2011 18:54:07 +0100 huffman remove constant 'ccpo.lub', re-use constant 'Sup' instead
Fri, 29 Oct 2010 11:04:41 +0200 krauss hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
Sat, 23 Oct 2010 23:39:37 +0200 krauss Complete_Partial_Order.thy: complete partial orders over arbitrary chains, with fixpoint theorem
less more (0) tip