| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 13:34:58 +0200 |
haftmann |
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 14:46:48 +0200 |
haftmann |
turned distinct and sorted into inductive predicates: yields nice induction principles for free
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 14:34:08 +0200 |
hoelzl |
Fixes lemma names
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 10:45:51 +0200 |
hoelzl |
Permutation implies bij function
|
file |
diff |
annotate
|
| Thu, 13 May 2010 14:34:05 +0200 |
nipkow |
Multiset: renamed, added and tuned lemmas;
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 09:15:10 +0100 |
haftmann |
switched notations for pointwise and multiset order
|
file |
diff |
annotate
|
| Sat, 07 Nov 2009 08:17:52 +0100 |
haftmann |
modernized primrec
|
file |
diff |
annotate
|
| Fri, 27 Mar 2009 12:22:01 +0100 |
haftmann |
tuned notoriously slow metis proof
|
file |
diff |
annotate
|
| Fri, 27 Mar 2009 10:05:11 +0100 |
haftmann |
normalized imports
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| Tue, 18 Mar 2008 20:33:31 +0100 |
wenzelm |
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
|
file |
diff |
annotate
|
| Fri, 15 Feb 2008 16:09:12 +0100 |
haftmann |
<= and < on nat no longer depend on wellfounded relations
|
file |
diff |
annotate
|
| Sat, 10 Nov 2007 18:36:07 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 18:18:39 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 08:31:12 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:28:13 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2006 18:51:13 +0200 |
wenzelm |
tuned syntax/abbreviations;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:37 +0200 |
wenzelm |
tuned presentation;
|
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
|
| Thu, 24 Jun 2004 17:54:53 +0200 |
paulson |
Norbert Voelker
|
file |
diff |
annotate
|
| Thu, 06 May 2004 14:14:18 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Fri, 16 Feb 2001 13:37:21 +0100 |
paulson |
Blast bug fix made old proof too slow
|
file |
diff |
annotate
|
| Sun, 04 Feb 2001 19:42:54 +0100 |
wenzelm |
moved from Induct/ to Library/
|
file |
diff |
annotate
|