Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Lattices.thy
Wed, 10 Oct 2012 12:52:24 +0200 haftmann more explicit code equations file | diff | annotate
Mon, 12 Mar 2012 21:41:11 +0100 noschinl tuned proofs file | diff | annotate
Mon, 12 Mar 2012 15:11:24 +0100 noschinl tuned simpset file | diff | annotate
Sun, 26 Feb 2012 20:10:14 +0100 haftmann tuned syntax declarations; tuned structure file | diff | annotate
Sun, 26 Feb 2012 15:28:48 +0100 haftmann marked candidates for rule declarations file | diff | annotate
Thu, 23 Feb 2012 20:33:35 +0100 haftmann moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax file | diff | annotate
Tue, 21 Feb 2012 08:15:42 +0100 haftmann reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems file | diff | annotate
Sun, 19 Feb 2012 15:30:35 +0100 haftmann distributed lattice properties of predicates to places of instantiation file | diff | annotate
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs file | diff | annotate
Tue, 13 Sep 2011 16:22:01 +0200 noschinl tune proofs file | diff | annotate
Tue, 13 Sep 2011 16:21:48 +0200 noschinl tune simpset for Complete_Lattices file | diff | annotate
Fri, 09 Sep 2011 00:22:18 +0200 krauss added syntactic classes for "inf" and "sup" file | diff | annotate
Mon, 08 Aug 2011 22:33:36 +0200 haftmann move legacy candiates to bottom; marked candidates for default simp rules file | diff | annotate
Sun, 17 Jul 2011 22:24:08 +0200 haftmann more on complement file | diff | annotate
Sun, 10 Jul 2011 21:56:39 +0200 haftmann tuned notation file | diff | annotate
Wed, 08 Dec 2010 15:05:46 +0100 haftmann bot comes before top, inf before sup etc. file | diff | annotate
Wed, 08 Dec 2010 14:52:23 +0100 haftmann nice syntax for lattice INFI, SUPR; file | diff | annotate
Wed, 08 Dec 2010 13:34:50 +0100 haftmann primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq` file | diff | annotate
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s file | diff | annotate
Wed, 05 May 2010 09:24:41 +0200 haftmann tuned whitespace file | diff | annotate
Tue, 04 May 2010 08:55:43 +0200 haftmann locale predicates of classes carry a mandatory "class" prefix file | diff | annotate
Mon, 26 Apr 2010 15:14:14 +0200 Cezary Kaliszyk add bounded_lattice_bot and bounded_lattice_top type classes file | diff | annotate
Wed, 07 Apr 2010 19:17:10 +0200 ballarin Merged resolving conflicts NEWS and locale.ML. file | diff | annotate
Mon, 15 Feb 2010 01:27:06 +0100 ballarin Tuned interpretation proofs. file | diff | annotate
Sun, 28 Mar 2010 12:49:14 -0700 huffman add/change some lemmas about lattices file | diff | annotate
Thu, 11 Mar 2010 14:38:20 +0100 haftmann fixed typo file | diff | annotate
Mon, 22 Feb 2010 15:53:18 +0100 haftmann distributed theory Algebras to theories Groups and Lattices file | diff | annotate
Fri, 12 Feb 2010 14:28:01 +0100 haftmann tuned import order file | diff | annotate
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS file | diff | annotate
Thu, 28 Jan 2010 11:48:43 +0100 haftmann dropped mk_left_commute; use interpretation of locale abel_semigroup instead file | diff | annotate
Wed, 30 Dec 2009 10:24:53 +0100 krauss killed a few warnings file | diff | annotate
Sat, 05 Dec 2009 20:02:21 +0100 haftmann tuned lattices theory fragements; generlized some lemmas from sets to lattices file | diff | annotate
Wed, 30 Sep 2009 17:16:01 +0200 haftmann moved lemmas about sup on bool to Lattices.thy file | diff | annotate
Wed, 30 Sep 2009 17:09:06 +0200 haftmann tuned proofs file | diff | annotate
Tue, 22 Sep 2009 15:36:55 +0200 haftmann be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer file | diff | annotate
Mon, 14 Sep 2009 08:36:57 +0200 haftmann some lemmas about strict order in lattices file | diff | annotate
Thu, 03 Sep 2009 15:39:02 +0200 haftmann proper class syntax for sublocale class < expr file | diff | annotate
Fri, 28 Aug 2009 18:52:41 +0200 nipkow Turned "x <= y ==> sup x y = y" (and relatives) into simp rules file | diff | annotate
Sat, 25 Jul 2009 18:44:54 +0200 haftmann localized interpretation of min/max-lattice file | diff | annotate
Tue, 14 Jul 2009 15:54:19 +0200 haftmann refinement of lattice classes file | diff | annotate
Mon, 13 Jul 2009 08:25:43 +0200 haftmann removed outdated comment file | diff | annotate
Sat, 11 Jul 2009 21:33:01 +0200 haftmann added boolean_algebra type class; tuned lattice duals file | diff | annotate
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default; file | diff | annotate
Thu, 05 Mar 2009 08:23:09 +0100 haftmann moved complete_lattice to Set.thy file | diff | annotate
Wed, 21 Jan 2009 16:47:31 +0100 haftmann dropped ID file | diff | annotate
Fri, 16 Jan 2009 14:58:11 +0100 haftmann migrated class package to new locale implementation file | diff | annotate
Thu, 11 Dec 2008 18:30:26 +0100 ballarin Conversion of HOL-Main and ZF to new locales. file | diff | annotate
Mon, 17 Nov 2008 17:00:55 +0100 haftmann tuned unfold_locales invocation file | diff | annotate
Mon, 27 Oct 2008 16:15:47 +0100 haftmann sup_bot and inf_top file | diff | annotate
Fri, 24 Oct 2008 17:48:37 +0200 haftmann new classes "top" and "bot" file | diff | annotate
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code` file | diff | annotate
Fri, 25 Jul 2008 12:03:34 +0200 haftmann added class preorder file | diff | annotate
Wed, 07 May 2008 10:56:36 +0200 berghofe - Now imports Fun rather than Orderings file | diff | annotate
Fri, 07 Mar 2008 13:53:02 +0100 haftmann tuned proofs file | diff | annotate
Wed, 30 Jan 2008 10:57:46 +0100 haftmann dual orders and dual lattices file | diff | annotate
Fri, 30 Nov 2007 20:13:03 +0100 haftmann adjustions to due to instance target file | diff | annotate
Wed, 28 Nov 2007 09:01:37 +0100 haftmann dropped implicit assumption proof file | diff | annotate
Sat, 10 Nov 2007 23:03:52 +0100 wenzelm tuned specifications of 'notation'; file | diff | annotate
Fri, 26 Oct 2007 21:22:17 +0200 haftmann localized monotonicity; tuned syntax file | diff | annotate
Fri, 19 Oct 2007 19:45:29 +0200 haftmann antisymmetry not a default intro rule any longer file | diff | annotate
less more (0) -60 tip
isabelle