| Mon, 07 Jul 2008 08:47:17 +0200 |
haftmann |
absolute imports of HOL/*.thy theories
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 18:37:05 +0100 |
wenzelm |
avoid rebinding of existing facts;
|
file |
diff |
annotate
|
| Tue, 26 Feb 2008 20:38:17 +0100 |
haftmann |
some more primrec
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:54:44 +0100 |
haftmann |
dropped superfluous code theorems
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 18:30:11 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Wed, 06 Jun 2007 19:12:59 +0200 |
nipkow |
changed filter syntax from : to <-
|
file |
diff |
annotate
|
| Thu, 10 May 2007 10:21:44 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:33:09 +0200 |
haftmann |
slightly tuned
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:38 +0200 |
haftmann |
tuned: now using function package
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Mon, 11 Sep 2006 21:35:19 +0200 |
wenzelm |
induct method: renamed 'fixing' to 'arbitrary';
|
file |
diff |
annotate
|
| Tue, 28 Mar 2006 12:11:33 +0200 |
schirmer |
renamed map_val to map_ran
|
file |
diff |
annotate
|
| Tue, 28 Mar 2006 12:05:45 +0200 |
schirmer |
added map_val, superseding map_at and substitute
|
file |
diff |
annotate
|
| Thu, 23 Mar 2006 20:03:53 +0100 |
nipkow |
Converted translations to abbbreviations.
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 16:05:34 +0100 |
schirmer |
Added Library/AssocList.thy
|
file |
diff |
annotate
|