| Fri, 09 Sep 2011 00:22:18 +0200 |
krauss |
added syntactic classes for "inf" and "sup"
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 19:33:31 +0200 |
haftmann |
more concise definition for Inf, Sup on bool
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 08:07:22 +0200 |
haftmann |
tuned header
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 08:06:15 +0200 |
haftmann |
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
|
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
|
| Mon, 08 Aug 2011 22:11:00 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 19:30:18 +0200 |
haftmann |
dropped lemmas (Inf|Sup)_(singleton|binary)
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 19:21:11 +0200 |
haftmann |
dropped lemmas (Inf|Sup)_(singleton|binary)
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 11:47:41 -0700 |
huffman |
add lemmas INF_image, SUP_image
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 11:25:18 -0700 |
huffman |
declare {INF,SUP}_empty [simp]
|
file |
diff |
annotate
|
| Fri, 05 Aug 2011 23:06:54 +0200 |
haftmann |
tuned order: pushing INF and SUP to Inf and Sup
|
file |
diff |
annotate
|
| Fri, 05 Aug 2011 22:58:17 +0200 |
haftmann |
tuned order: pushing INF and SUP to Inf and Sup
|
file |
diff |
annotate
|
| Fri, 05 Aug 2011 22:45:57 +0200 |
haftmann |
generalized lemmas to complete lattices
|
file |
diff |
annotate
|
| Thu, 04 Aug 2011 19:29:52 +0200 |
haftmann |
solving duality problem for complete_distrib_lattice; tuned
|
file |
diff |
annotate
|
| Thu, 04 Aug 2011 07:33:08 +0200 |
haftmann |
tuned orthography
|
file |
diff |
annotate
|
| Thu, 04 Aug 2011 07:31:59 +0200 |
haftmann |
avoid yet unknown fact antiquotation
|
file |
diff |
annotate
|
| Wed, 03 Aug 2011 23:21:52 +0200 |
haftmann |
class complete_distrib_lattice
|
file |
diff |
annotate
|
| Sun, 24 Jul 2011 21:27:25 +0200 |
haftmann |
more coherent structure in and across theories
|
file |
diff |
annotate
|
| Fri, 22 Jul 2011 07:33:29 +0200 |
haftmann |
dropped errorneous hint
|
file |
diff |
annotate
|
| Thu, 21 Jul 2011 22:47:13 +0200 |
haftmann |
moved some lemmas
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 22:14:39 +0200 |
haftmann |
class complete_linorder
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 21:52:34 +0200 |
haftmann |
proof tuning
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 21:49:39 +0200 |
haftmann |
generalization; various notation and proof tuning
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 21:34:01 +0200 |
haftmann |
avoid misunderstandable names
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 21:15:51 +0200 |
haftmann |
moved lemmas to appropriate theory
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 22:24:08 +0200 |
haftmann |
more on complement
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 20:57:56 +0200 |
haftmann |
more consistent theorem names
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 20:46:51 +0200 |
haftmann |
more lemmas about SUP
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 20:29:54 +0200 |
haftmann |
structuring duals together
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 20:23:33 +0200 |
haftmann |
more lemmas about Sup
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 19:55:17 +0200 |
haftmann |
generalized INT_anti_mono
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 19:48:02 +0200 |
haftmann |
moving UNIV = ... equations to their proper theories
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 15:15:58 +0200 |
haftmann |
further generalization from sets to complete lattices
|
file |
diff |
annotate
|
| Sat, 16 Jul 2011 22:28:35 +0200 |
haftmann |
generalized some lemmas
|
file |
diff |
annotate
|
| Sat, 16 Jul 2011 22:04:02 +0200 |
haftmann |
consolidated bot and top classes, tuned notation
|
file |
diff |
annotate
|
| Sat, 16 Jul 2011 21:53:50 +0200 |
haftmann |
tuned notation
|
file |
diff |
annotate
|
| Thu, 14 Jul 2011 17:14:54 +0200 |
haftmann |
tuned notation and proofs
|
file |
diff |
annotate
|
| Thu, 14 Jul 2011 00:20:43 +0200 |
haftmann |
tuned lemma positions and proofs
|
file |
diff |
annotate
|
| Thu, 14 Jul 2011 00:16:41 +0200 |
haftmann |
tuned notation
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 19:43:12 +0200 |
haftmann |
moved lemmas bot_less and less_top to classes bot and top respectively
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 07:26:31 +0200 |
haftmann |
more generalization towards complete lattices
|
file |
diff |
annotate
|
| Sun, 10 Jul 2011 22:42:53 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sun, 10 Jul 2011 22:17:33 +0200 |
haftmann |
tuned notation
|
file |
diff |
annotate
|
| Sun, 10 Jul 2011 22:11:32 +0200 |
haftmann |
tuned notation
|
file |
diff |
annotate
|
| Sun, 10 Jul 2011 21:56:39 +0200 |
haftmann |
tuned notation
|
file |
diff |
annotate
|
| Sun, 10 Jul 2011 15:45:35 +0200 |
haftmann |
tuned proofs and notation
|
file |
diff |
annotate
|
| Sun, 10 Jul 2011 14:26:07 +0200 |
haftmann |
more succinct proofs
|
file |
diff |
annotate
|
| Sun, 10 Jul 2011 14:14:19 +0200 |
haftmann |
more succinct proofs
|
file |
diff |
annotate
|
| 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
|