| Tue, 20 Sep 2011 05:48:23 +0200 |
nipkow |
Updated IMP to use new induction method
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 22:47:26 +0200 |
nipkow |
Made comments text
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 22:42:37 +0200 |
nipkow |
Fixed denotational semantics
|
file |
diff |
annotate
|
| Wed, 30 Mar 2011 23:26:40 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Sun, 16 Jan 2011 15:53:03 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Thu, 10 Dec 2009 17:34:18 +0000 |
paulson |
streamlined proofs
|
file |
diff |
annotate
|
| Mon, 27 Jul 2009 21:47:41 +0200 |
krauss |
"more standard" argument order of relation composition (op O)
|
file |
diff |
annotate
|
| Wed, 25 Jun 2008 22:01:34 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:14:51 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Fri, 13 Oct 2006 18:15:18 +0200 |
berghofe |
Adapted to changes in FixedPoint theory.
|
file |
diff |
annotate
|
| Mon, 11 Sep 2006 21:35:19 +0200 |
wenzelm |
induct method: renamed 'fixing' to 'arbitrary';
|
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
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
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
|
| Tue, 04 Jul 2000 10:54:46 +0200 |
oheimb |
disambiguated := ; added Examples (factorial)
|
file |
diff |
annotate
|
| Fri, 02 Oct 1998 14:28:39 +0200 |
nipkow |
id <-> Id
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:03:20 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
| Wed, 06 May 1998 11:46:00 +0200 |
nipkow |
Changed [/] to [:=] and removed actual definition.
|
file |
diff |
annotate
|
| Sun, 30 Mar 1997 13:40:38 +0200 |
nipkow |
Replaced (s,t) : id by s=t.
|
file |
diff |
annotate
|
| Sat, 27 Apr 1996 18:47:31 +0200 |
nipkow |
A completely new version of IMP.
|
file |
diff |
annotate
|
| Wed, 07 Feb 1996 12:22:32 +0100 |
nipkow |
Modified datatype com.
|
file |
diff |
annotate
|
| Mon, 05 Feb 1996 21:29:06 +0100 |
clasohm |
expanded tabs; incorporated Konrad's changes
|
file |
diff |
annotate
|
| Wed, 29 Nov 1995 17:01:41 +0100 |
clasohm |
removed quotes from consts and syntax sections
|
file |
diff |
annotate
|
| Wed, 21 Jun 1995 15:47:10 +0200 |
clasohm |
removed \...\ inside strings
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:04:16 +0100 |
clasohm |
new version of HOL/IMP with curried function application
|
file |
diff |
annotate
|