Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
Mon, 02 Mar 2009 16:53:55 +0100 |
nipkow |
name changes
|
file |
diff |
annotate
|
Wed, 11 Jul 2007 11:14:51 +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
|
Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
Sat, 27 May 2006 17:42:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 22 Dec 2005 00:28:43 +0100 |
wenzelm |
tuned induct proofs;
|
file |
diff |
annotate
|
Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
Thu, 02 Sep 2004 16:52:21 +0200 |
paulson |
new example of a quotiented nested data type
|
file |
diff |
annotate
|
Wed, 01 Sep 2004 15:04:01 +0200 |
paulson |
new "respects" syntax for quotienting
|
file |
diff |
annotate
|
Fri, 20 Aug 2004 12:25:20 +0200 |
paulson |
new examples
|
file |
diff |
annotate
|
Fri, 06 Aug 2004 16:55:14 +0200 |
nipkow |
undid UN/INT syntax
|
file |
diff |
annotate
|
Fri, 23 Apr 2004 11:04:07 +0200 |
paulson |
congruent2 now allows different equiv relations
|
file |
diff |
annotate
|
Wed, 14 Apr 2004 14:13:05 +0200 |
kleing |
use more symbols in HTML output
|
file |
diff |
annotate
|
Thu, 08 Apr 2004 15:47:44 +0200 |
paulson |
freeness theorems and induction rule
|
file |
diff |
annotate
|
Wed, 07 Apr 2004 14:25:48 +0200 |
paulson |
IsaMakefile
|
file |
diff |
annotate
|