src/HOL/HOLCF/UpperPD.thy
Sun, 25 Aug 2024 21:10:01 +0200 wenzelm more markup for syntax consts;
Tue, 20 Feb 2018 22:25:23 +0100 wenzelm tuned proofs -- prefer explicit names for facts from 'interpret';
Wed, 13 Jan 2016 23:07:06 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 30 Dec 2015 21:23:38 +0100 wenzelm clarified print modes;
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Sun, 02 Nov 2014 17:16:01 +0100 wenzelm modernized header;
Sat, 23 Mar 2013 20:50:39 +0100 haftmann fundamental revision of big operators on sets
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Tue, 29 Mar 2011 17:47:11 +0200 wenzelm tuned headers;
Sat, 08 Jan 2011 11:18:09 -0800 huffman use proper syntactic types for 'syntax' commands
Tue, 04 Jan 2011 15:32:56 -0800 huffman change some lemma names containing 'UU' to 'bottom'
Fri, 24 Dec 2010 14:26:10 -0800 huffman remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
Thu, 23 Dec 2010 11:51:59 -0800 huffman changed syntax of powerdomain binary union operators
Wed, 22 Dec 2010 18:24:04 -0800 huffman rename function ideal_completion.basis_fun to ideal_completion.extension
Sun, 19 Dec 2010 06:59:01 -0800 huffman minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
Sun, 19 Dec 2010 06:39:19 -0800 huffman powerdomain theories require class 'bifinite' instead of 'domain'
Sun, 19 Dec 2010 06:34:41 -0800 huffman type 'defl' takes a type parameter again (cf. b525988432e9)
Sun, 19 Dec 2010 05:15:31 -0800 huffman reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
Fri, 17 Dec 2010 16:43:45 -0800 huffman renamed CompactBasis.thy to Compact_Basis.thy
Sat, 11 Dec 2010 11:26:37 -0800 huffman xsymbol notation for powerdomain types
Sat, 11 Dec 2010 10:35:40 -0800 huffman new powerdomain lemmas
Mon, 06 Dec 2010 14:17:35 -0800 huffman add set-union-like syntax for powerdomain bind operators
Wed, 01 Dec 2010 20:29:39 -0800 huffman reformulate lemma preorder.ex_ideal, and use it for typedefs
Sat, 27 Nov 2010 16:08:10 -0800 huffman moved directory src/HOLCF to src/HOL/HOLCF;
less more (0) tip