| 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
|