| Mon, 18 Jul 2011 21:34:01 +0200 |
avoid misunderstandable names
|
file | diff | annotate |
| Mon, 18 Jul 2011 21:15:51 +0200 |
moved lemmas to appropriate theory
|
file | diff | annotate |
| Sun, 17 Jul 2011 22:24:08 +0200 |
more on complement
|
file | diff | annotate |
| Sun, 17 Jul 2011 20:57:56 +0200 |
more consistent theorem names
|
file | diff | annotate |
| Sun, 17 Jul 2011 20:46:51 +0200 |
more lemmas about SUP
|
file | diff | annotate |
| Sun, 17 Jul 2011 20:29:54 +0200 |
structuring duals together
|
file | diff | annotate |
| Sun, 17 Jul 2011 20:23:33 +0200 |
more lemmas about Sup
|
file | diff | annotate |
| Sun, 17 Jul 2011 19:55:17 +0200 |
generalized INT_anti_mono
|
file | diff | annotate |
| Sun, 17 Jul 2011 19:48:02 +0200 |
moving UNIV = ... equations to their proper theories
|
file | diff | annotate |
| Sun, 17 Jul 2011 15:15:58 +0200 |
further generalization from sets to complete lattices
|
file | diff | annotate |
| Sat, 16 Jul 2011 22:28:35 +0200 |
generalized some lemmas
|
file | diff | annotate |
| Sat, 16 Jul 2011 22:04:02 +0200 |
consolidated bot and top classes, tuned notation
|
file | diff | annotate |
| Sat, 16 Jul 2011 21:53:50 +0200 |
tuned notation
|
file | diff | annotate |
| Thu, 14 Jul 2011 17:14:54 +0200 |
tuned notation and proofs
|
file | diff | annotate |
| Thu, 14 Jul 2011 00:20:43 +0200 |
tuned lemma positions and proofs
|
file | diff | annotate |
| Thu, 14 Jul 2011 00:16:41 +0200 |
tuned notation
|
file | diff | annotate |
| Wed, 13 Jul 2011 19:43:12 +0200 |
moved lemmas bot_less and less_top to classes bot and top respectively
|
file | diff | annotate |
| Wed, 13 Jul 2011 07:26:31 +0200 |
more generalization towards complete lattices
|
file | diff | annotate |
| Sun, 10 Jul 2011 22:42:53 +0200 |
tuned proofs
|
file | diff | annotate |
| Sun, 10 Jul 2011 22:17:33 +0200 |
tuned notation
|
file | diff | annotate |
| Sun, 10 Jul 2011 22:11:32 +0200 |
tuned notation
|
file | diff | annotate |
| Sun, 10 Jul 2011 21:56:39 +0200 |
tuned notation
|
file | diff | annotate |
| Sun, 10 Jul 2011 15:45:35 +0200 |
tuned proofs and notation
|
file | diff | annotate |
| Sun, 10 Jul 2011 14:26:07 +0200 |
more succinct proofs
|
file | diff | annotate |
| Sun, 10 Jul 2011 14:14:19 +0200 |
more succinct proofs
|
file | diff | annotate |
| Fri, 08 Apr 2011 13:31:16 +0200 |
explicit structure Syntax_Trans;
|
file | diff | annotate |
| Mon, 14 Mar 2011 14:37:36 +0100 |
add lemmas for SUP and INF
|
file | diff | annotate |
| Wed, 08 Dec 2010 15:05:46 +0100 |
bot comes before top, inf before sup etc.
|
file | diff | annotate |
| Wed, 08 Dec 2010 14:52:23 +0100 |
nice syntax for lattice INFI, SUPR;
|
file | diff | annotate |
| Thu, 02 Dec 2010 14:34:58 +0100 |
Move SUP_commute, SUP_less_iff to HOL image;
|
file | diff | annotate |
| Fri, 26 Nov 2010 16:28:34 +0100 |
prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
|
file | diff | annotate |
| Mon, 13 Sep 2010 11:13:15 +0200 |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file | diff | annotate |
| Tue, 24 Aug 2010 14:41:37 +0200 |
moved generic lemmas in Probability to HOL
|
file | diff | annotate |
| Mon, 12 Jul 2010 10:48:37 +0200 |
dropped superfluous [code del]s
|
file | diff | annotate |
| Tue, 04 May 2010 08:55:43 +0200 |
locale predicates of classes carry a mandatory "class" prefix
|
file | diff | annotate |
| Mon, 26 Apr 2010 09:37:46 -0700 |
fix syntax precedence declarations for UNION, INTER, SUP, INF
|
file | diff | annotate |
| Thu, 18 Mar 2010 12:58:52 +0100 |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file | diff | annotate |
| Sat, 06 Mar 2010 08:08:30 -0800 |
add some lemmas about complete lattices
|
file | diff | annotate |
| Thu, 11 Feb 2010 23:00:22 +0100 |
modernized translations;
|
file | diff | annotate |
| Sat, 05 Dec 2009 20:02:21 +0100 |
tuned lattices theory fragements; generlized some lemmas from sets to lattices
|
file | diff | annotate |
| Tue, 06 Oct 2009 15:51:34 +0200 |
added syntactic Inf and Sup
|
file | diff | annotate |
| Thu, 24 Sep 2009 18:29:28 +0200 |
added dual for complete lattice
|
file | diff | annotate |
| Tue, 22 Sep 2009 15:36:55 +0200 |
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 |
| Fri, 18 Sep 2009 14:09:38 +0200 |
INTER and UNION are mere abbreviations for INFI and SUPR
|
file | diff | annotate |
| Wed, 16 Sep 2009 13:43:05 +0200 |
Inter and Union are mere abbreviations for Inf and Sup
|
file | diff | annotate |
| Fri, 28 Aug 2009 18:52:41 +0200 |
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
|
file | diff | annotate |
| Wed, 22 Jul 2009 18:02:10 +0200 |
moved complete_lattice &c. into separate theory
|
file | diff | annotate | base |