| Mon, 27 Sep 2004 10:27:34 +0200 |
ballarin |
Modified locales: improved implementation of "includes".
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Fri, 06 Aug 2004 16:55:14 +0200 |
nipkow |
undid UN/INT syntax
|
file |
diff |
annotate
|
| Tue, 03 Aug 2004 13:48:00 +0200 |
paulson |
new simprules Int_subset_iff and Un_subset_iff
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Sat, 29 May 2004 15:11:43 +0200 |
wenzelm |
\<^bsub>/\<^esub> syntax: unbreakable block;
|
file |
diff |
annotate
|
| Fri, 28 May 2004 11:19:15 +0200 |
paulson |
new theorem Collect_imp_eq
|
file |
diff |
annotate
|
| Wed, 26 May 2004 14:57:06 +0200 |
nipkow |
Corrected printer bug for bounded quantifiers Q x<=y. P
|
file |
diff |
annotate
|
| Mon, 17 May 2004 11:02:16 +0200 |
mehta |
lemma disjoint_int_union removed - too special
|
file |
diff |
annotate
|
| Thu, 13 May 2004 16:02:29 +0200 |
mehta |
New simp rules added:
|
file |
diff |
annotate
|
| Sat, 01 May 2004 22:04:14 +0200 |
wenzelm |
improved subscript syntax;
|
file |
diff |
annotate
|
| Wed, 14 Apr 2004 14:13:05 +0200 |
kleing |
use more symbols in HTML output
|
file |
diff |
annotate
|
| Tue, 13 Apr 2004 09:42:40 +0200 |
ballarin |
Various changes to HOL-Algebra;
|
file |
diff |
annotate
|
| Wed, 24 Mar 2004 10:50:29 +0100 |
paulson |
streamlined treatment of quotients for the integers
|
file |
diff |
annotate
|
| Thu, 19 Feb 2004 15:57:34 +0100 |
ballarin |
Efficient, graph-based reasoner for linear and partial orders.
|
file |
diff |
annotate
|
| Wed, 11 Feb 2004 01:26:15 +0100 |
nipkow |
Modified UN and INT xsymbol syntax: made index subscript
|
file |
diff |
annotate
|
| Thu, 01 Jan 2004 21:47:07 +0100 |
paulson |
conversion of Real/PReal to Isar script;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2003 04:28:45 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 26 Sep 2003 10:34:57 +0200 |
paulson |
misc tidying
|
file |
diff |
annotate
|
| Fri, 11 Jul 2003 14:11:56 +0200 |
oheimb |
added rev_ballE
|
file |
diff |
annotate
|
| Mon, 17 Mar 2003 17:37:20 +0100 |
paulson |
moved one proof, added another
|
file |
diff |
annotate
|
| Fri, 14 Mar 2003 10:30:15 +0100 |
paulson |
new UN/INT simprules
|
file |
diff |
annotate
|
| Tue, 11 Mar 2003 15:19:27 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 26 Feb 2003 10:44:54 +0100 |
paulson |
new lemma
|
file |
diff |
annotate
|
| Tue, 25 Feb 2003 12:42:08 +0100 |
nipkow |
Undid eta change for UN/INT.
|
file |
diff |
annotate
|
| Sun, 16 Feb 2003 12:16:07 +0100 |
paulson |
new theorem Compl_partition2
|
file |
diff |
annotate
|
| Sun, 22 Dec 2002 15:02:40 +0100 |
nipkow |
removed some problems with print translations
|
file |
diff |
annotate
|
| Sun, 22 Dec 2002 10:43:43 +0100 |
nipkow |
added print translations tha avoid eta contraction for important binders.
|
file |
diff |
annotate
|
| Fri, 18 Oct 2002 09:53:02 +0200 |
nipkow |
Added a few thms about UN/INT/{}/UNIV
|
file |
diff |
annotate
|
| Thu, 03 Oct 2002 10:34:51 +0200 |
paulson |
added the new elim rule psubsetE
|
file |
diff |
annotate
|
| Fri, 30 Aug 2002 16:42:45 +0200 |
paulson |
removal of blast.overloaded
|
file |
diff |
annotate
|
| Tue, 06 Aug 2002 11:22:05 +0200 |
wenzelm |
sane interface for simprocs;
|
file |
diff |
annotate
|
| Wed, 24 Jul 2002 22:15:55 +0200 |
wenzelm |
simplified locale predicates;
|
file |
diff |
annotate
|
| Tue, 07 May 2002 19:54:04 +0200 |
wenzelm |
rev_bexI [intro?];
|
file |
diff |
annotate
|
| Mon, 06 May 2002 09:42:20 +0200 |
nipkow |
Added insert_disjoint and disjoint_insert [simp], and simplified proofs
|
file |
diff |
annotate
|
| Mon, 25 Feb 2002 20:48:14 +0100 |
wenzelm |
clarified syntax of ``long'' statements: fixes/assumes/shows;
|
file |
diff |
annotate
|
| Sat, 16 Feb 2002 20:59:34 +0100 |
wenzelm |
converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
|
file |
diff |
annotate
|
| Fri, 04 Jan 2002 19:29:30 +0100 |
wenzelm |
tuned ``syntax (output)'';
|
file |
diff |
annotate
|
| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Wed, 21 Nov 2001 00:33:04 +0100 |
wenzelm |
theory Inverse_Image converted and moved to Set;
|
file |
diff |
annotate
|
| Fri, 09 Nov 2001 00:09:47 +0100 |
wenzelm |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:33:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 02 Nov 2001 22:01:58 +0100 |
wenzelm |
theory Calculation move to Set;
|
file |
diff |
annotate
|
| Tue, 30 Oct 2001 13:43:26 +0100 |
wenzelm |
lemma Least_mono moved from Typedef.thy to Set.thy;
|
file |
diff |
annotate
|
| Sun, 28 Oct 2001 22:59:12 +0100 |
wenzelm |
converted theory "Set";
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 20:02:30 +0200 |
wenzelm |
removed Ord;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2001 16:46:19 +0100 |
nipkow |
fixed set comprehension print translation
|
file |
diff |
annotate
|
| Tue, 09 Jan 2001 15:22:13 +0100 |
nipkow |
`` -> and ``` -> ``
|
file |
diff |
annotate
|
| Tue, 03 Oct 2000 01:14:52 +0200 |
wenzelm |
range declared as syntax;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2000 14:42:21 +0200 |
wenzelm |
fixed \<Union>, \<Inter> syntax;
|
file |
diff |
annotate
|
| Fri, 28 Jan 2000 11:22:02 +0100 |
oheimb |
beautified spacing for binders with symbols syntax, analogous to HOL.thy
|
file |
diff |
annotate
|
| Thu, 11 Nov 1999 10:25:17 +0100 |
paulson |
new-style infix declaration for "image"
|
file |
diff |
annotate
|
| Thu, 26 Aug 1999 11:32:39 +0200 |
paulson |
a little tidying; also FIXED BAD TYPE in INTER1, UNION1
|
file |
diff |
annotate
|
| Tue, 17 Aug 1999 22:13:23 +0200 |
wenzelm |
replaced HOL_quantifiers flag by "HOL" print mode;
|
file |
diff |
annotate
|
| Wed, 18 Nov 1998 15:10:46 +0100 |
paulson |
Finally removing "Compl" from HOL
|
file |
diff |
annotate
|
| Fri, 30 Oct 1998 10:45:08 +0100 |
paulson |
Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed
|
file |
diff |
annotate
|
| Tue, 15 Sep 1998 15:10:38 +0200 |
paulson |
From Compl(A) to -A
|
file |
diff |
annotate
|
| Wed, 05 Aug 1998 10:59:51 +0200 |
paulson |
Removal of "disjoint" translation
|
file |
diff |
annotate
|
| Tue, 04 Aug 1998 09:22:07 +0200 |
wenzelm |
fixed disjount translation;
|
file |
diff |
annotate
|