| Fri, 05 May 2006 17:17:21 +0200 |
krauss |
First usable version of the new function definition package (HOL/function_packake/...).
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:06 +0200 |
wenzelm |
refined 'abbreviation';
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 21:12:00 +0100 |
wenzelm |
new-style definitions/abbreviations;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:21 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2005 19:20:56 +0100 |
wenzelm |
tuned induct proofs;
|
file |
diff |
annotate
|
| Fri, 07 Oct 2005 20:41:10 +0200 |
nipkow |
changes due to new neq_simproc in simpdata.ML
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:37 +0200 |
wenzelm |
tuned presentation;
|
file |
diff |
annotate
|
| Sun, 28 Aug 2005 16:04:45 +0200 |
wenzelm |
tuned some proofs;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2005 12:02:49 +0200 |
kleing |
intersection
|
file |
diff |
annotate
|
| Thu, 28 Apr 2005 09:21:15 +0200 |
kleing |
some more lemmas about multiset_of
|
file |
diff |
annotate
|
| Sat, 26 Mar 2005 00:00:56 +0100 |
kleing |
fixed typo (multiset_append)
|
file |
diff |
annotate
|
| Sun, 12 Dec 2004 16:25:47 +0100 |
nipkow |
REorganized Finite_Set
|
file |
diff |
annotate
|
| Tue, 23 Nov 2004 16:43:03 +0100 |
nipkow |
renamed 1 lemmas
|
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
|
| Thu, 22 Jul 2004 10:33:26 +0200 |
paulson |
new material courtesy of Norbert Voelker
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
| Sun, 09 May 2004 23:04:36 +0200 |
obua |
replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
|
file |
diff |
annotate
|
| Thu, 06 May 2004 14:14:18 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Sat, 01 May 2004 22:01:57 +0200 |
wenzelm |
tuned instance statements;
|
file |
diff |
annotate
|
| Mon, 08 Mar 2004 12:17:43 +0100 |
ballarin |
Bug-fixes for transitivity reasoner.
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 16:14:02 +0200 |
berghofe |
Adapted to new simplifier.
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 15:44:21 +0200 |
nipkow |
modified induct method
|
file |
diff |
annotate
|
| Thu, 06 Dec 2001 00:40:19 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 11:54:22 +0200 |
paulson |
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Wed, 03 Oct 2001 20:54:16 +0200 |
wenzelm |
tuned parentheses in relational expressions;
|
file |
diff |
annotate
|
| Tue, 04 Sep 2001 21:10:57 +0200 |
wenzelm |
renamed "antecedent" case to "rule_context";
|
file |
diff |
annotate
|
| Mon, 06 Aug 2001 13:43:24 +0200 |
nipkow |
turned translation for 1::nat into def.
|
file |
diff |
annotate
|
| Thu, 21 Dec 2000 10:16:07 +0100 |
paulson |
re-orientation of 0=... (no idea why the backslashes have changed too)
|
file |
diff |
annotate
|
| Sat, 04 Nov 2000 18:41:37 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 23 Oct 2000 22:17:55 +0200 |
wenzelm |
intro_classes by default;
|
file |
diff |
annotate
|
| Thu, 19 Oct 2000 21:22:44 +0200 |
wenzelm |
improved typedef;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2000 23:28:33 +0200 |
wenzelm |
Multisets (from HOL/Induct/Multiset and friends);
|
file |
diff |
annotate
|