| Wed, 12 Jan 2011 17:19:50 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Sat, 30 Jan 2010 17:03:46 +0100 |
berghofe |
Adapted to changes in cases method.
|
file |
diff |
annotate
|
| Thu, 10 Dec 2009 17:34:18 +0000 |
paulson |
streamlined proofs
|
file |
diff |
annotate
|
| Mon, 20 Apr 2009 09:32:07 +0200 |
haftmann |
power operation on functions with syntax o^; power operation on relations with syntax ^^
|
file |
diff |
annotate
|
| Wed, 25 Jun 2008 22:01:34 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Tue, 08 Jan 2008 11:37:28 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:14:51 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 18:30:11 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:35:28 +0100 |
berghofe |
Adapted to changes in Transitive_Closure theory.
|
file |
diff |
annotate
|
| Mon, 11 Sep 2006 21:35:19 +0200 |
wenzelm |
induct method: renamed 'fixing' to 'arbitrary';
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 15:44:39 +0100 |
paulson |
Provers/classical: stricter checks to ensure that supplied intro, dest and
|
file |
diff |
annotate
|
| Wed, 21 Dec 2005 12:02:57 +0100 |
paulson |
removed or modified some instances of [iff]
|
file |
diff |
annotate
|
| Thu, 08 Dec 2005 20:15:50 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Wed, 14 Apr 2004 14:13:05 +0200 |
kleing |
use more symbols in HTML output
|
file |
diff |
annotate
|
| Tue, 27 Aug 2002 11:03:05 +0200 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 20 Dec 2001 18:22:44 +0100 |
nipkow |
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
|
file |
diff |
annotate
|
| Wed, 19 Dec 2001 00:26:04 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 09 Dec 2001 15:26:13 +0100 |
kleing |
tuned
|
file |
diff |
annotate
|
| Sun, 09 Dec 2001 14:35:36 +0100 |
kleing |
converted to Isar
|
file |
diff |
annotate
|
| Sun, 16 Jul 2000 20:55:17 +0200 |
wenzelm |
fixed tuple translations;
|
file |
diff |
annotate
|
| Tue, 04 Jul 2000 10:54:46 +0200 |
oheimb |
disambiguated := ; added Examples (factorial)
|
file |
diff |
annotate
|
| Wed, 24 Nov 1999 12:12:36 +0100 |
nipkow |
Basis now Main.
|
file |
diff |
annotate
|
| Fri, 13 Nov 1998 13:28:23 +0100 |
paulson |
the type of @evalcn was wrong
|
file |
diff |
annotate
|
| Fri, 08 May 1998 15:45:01 +0200 |
wenzelm |
fixed translations;
|
file |
diff |
annotate
|
| Wed, 06 May 1998 11:46:00 +0200 |
nipkow |
Changed [/] to [:=] and removed actual definition.
|
file |
diff |
annotate
|
| Mon, 30 Mar 1998 21:03:14 +0200 |
oheimb |
removed superfluous translations
|
file |
diff |
annotate
|
| Thu, 06 Jun 1996 14:39:44 +0200 |
paulson |
Quotes now optional around inductive set
|
file |
diff |
annotate
|
| Mon, 29 Apr 1996 20:15:33 +0200 |
nipkow |
Streamlined syntax: -(n)-> is now -n->.
|
file |
diff |
annotate
|
| Mon, 29 Apr 1996 15:48:27 +0200 |
nipkow |
Natural and Transition semantics.
|
file |
diff |
annotate
|