| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:36 +0100 |
hoelzl |
add lemmas for SUP and INF
|
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
|
| Thu, 02 Dec 2010 14:34:58 +0100 |
hoelzl |
Move SUP_commute, SUP_less_iff to HOL image;
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 16:28:34 +0100 |
wenzelm |
prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
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 |
hoelzl |
moved generic lemmas in Probability to HOL
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
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 09:37:46 -0700 |
huffman |
fix syntax precedence declarations for UNION, INTER, SUP, INF
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 08:08:30 -0800 |
huffman |
add some lemmas about complete lattices
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
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
|
| Tue, 06 Oct 2009 15:51:34 +0200 |
haftmann |
added syntactic Inf and Sup
|
file |
diff |
annotate
|
| Thu, 24 Sep 2009 18:29:28 +0200 |
haftmann |
added dual for complete lattice
|
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
|
| Fri, 18 Sep 2009 14:09:38 +0200 |
haftmann |
INTER and UNION are mere abbreviations for INFI and SUPR
|
file |
diff |
annotate
|
| Wed, 16 Sep 2009 13:43:05 +0200 |
haftmann |
Inter and Union are mere abbreviations for Inf and Sup
|
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
|
| Wed, 22 Jul 2009 18:02:10 +0200 |
haftmann |
moved complete_lattice &c. into separate theory
|
file |
diff |
annotate
| base
|