src/HOL/Complete_Partial_Order.thy
Wed, 25 May 2022 14:39:46 +0200 desharna move monotone from Complete_Partial_Order to Orderings
Thu, 11 Mar 2021 07:05:38 +0000 haftmann avoid name clash
Tue, 16 Feb 2021 17:12:02 +0000 paulson tidied up a few ugly proofs
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sat, 01 Oct 2016 17:16:35 +0200 wenzelm clarified lfp/gfp statements and proofs;
Tue, 06 Sep 2016 21:09:18 +0200 wenzelm clarified proof: save 1-2s CPU time;
Fri, 05 Aug 2016 18:14:28 +0200 wenzelm misc tuning and modernization;
Thu, 07 Jan 2016 15:53:39 +0100 wenzelm more uniform treatment of package internals;
Mon, 16 Nov 2015 17:00:11 +0100 Andreas Lochbihler export internal definition
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
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