| Sun, 27 Nov 2011 13:31:52 +0100 |
nipkow |
simplified Collecting1 and renamed: step -> step', step_cs -> step
|
file |
diff |
annotate
|
| Wed, 28 Sep 2011 09:55:11 +0200 |
nipkow |
Added Hoare-like Abstract Interpretation
|
file |
diff |
annotate
|
| Wed, 28 Sep 2011 08:51:55 +0200 |
nipkow |
moved IMP/AbsInt stuff into subdirectory Abs_Int_Den
|
file |
diff |
annotate
|
| Thu, 15 Sep 2011 09:44:08 +0200 |
nipkow |
revised AbsInt and added widening and narrowing
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 19:25:18 +0200 |
nipkow |
Added Abstract Interpretation theories
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 16:47:55 +0200 |
kleing |
import constant folding theory into IMP
|
file |
diff |
annotate
|
| Fri, 17 Jun 2011 20:38:43 +0200 |
kleing |
IMP compiler with int, added reverse soundness direction
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 16:29:38 +0200 |
kleing |
imported rest of new IMP
|
file |
diff |
annotate
|
| Thu, 02 Jun 2011 10:10:23 +0200 |
nipkow |
Added typed IMP
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 22:42:37 +0200 |
nipkow |
Fixed denotational semantics
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 21:35:34 +0200 |
nipkow |
Replacing old IMP with new Semantics material
|
file |
diff |
annotate
|
| Sun, 16 Jan 2011 15:53:03 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Fri, 12 Mar 2010 18:42:56 +0100 |
nipkow |
Reorganized Hoare logic theories; added Hoare_Den
|
file |
diff |
annotate
|
| Fri, 12 Mar 2010 15:48:18 +0100 |
nipkow |
Added Hoare_Op.thy
|
file |
diff |
annotate
|
| Tue, 14 Oct 2008 13:23:31 +0200 |
nipkow |
Added liveness analysis
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 22:21:20 +0200 |
wenzelm |
simultaneous use_thys;
|
file |
diff |
annotate
|
| Fri, 26 Apr 2002 11:47:01 +0200 |
nipkow |
New machine architecture and other direction of compiler proof.
|
file |
diff |
annotate
|
| Thu, 26 Oct 2000 14:52:41 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 07 Jul 2000 16:48:12 +0200 |
oheimb |
added dependency caveat
|
file |
diff |
annotate
|
| Fri, 07 Jul 2000 16:47:56 +0200 |
oheimb |
added dependency caveat
|
file |
diff |
annotate
|
| Tue, 04 Jul 2000 10:54:46 +0200 |
oheimb |
disambiguated := ; added Examples (factorial)
|
file |
diff |
annotate
|
| Tue, 30 May 2000 16:08:38 +0200 |
wenzelm |
cleaned up;
|
file |
diff |
annotate
|
| Thu, 11 Mar 1999 13:20:35 +0100 |
wenzelm |
removed foo_build_completed -- now handled by session management (via usedir);
|
file |
diff |
annotate
|
| Fri, 19 Dec 1997 10:28:33 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 27 Apr 1996 18:47:31 +0200 |
nipkow |
A completely new version of IMP.
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Tue, 23 Jan 1996 10:59:35 +0100 |
nipkow |
Added a verified verification-condition generator.
|
file |
diff |
annotate
|
| Tue, 21 Nov 1995 12:43:09 +0100 |
clasohm |
removed make_chart;
|
file |
diff |
annotate
|
| Fri, 17 Nov 1995 13:15:19 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 24 Oct 1995 14:50:24 +0100 |
clasohm |
added calls of init_html and make_chart
|
file |
diff |
annotate
|
| Thu, 29 Jun 1995 12:48:48 +0200 |
clasohm |
renamed CHOL to HOL
|
file |
diff |
annotate
|
| Mon, 10 Apr 1995 08:47:43 +0200 |
nipkow |
Removed the "exit 1" calls, since now the Makefile does them.
|
file |
diff |
annotate
|
| Tue, 14 Mar 1995 09:47:28 +0100 |
nipkow |
added exit 1
|
file |
diff |
annotate
|
| Tue, 07 Mar 1995 14:57:37 +0100 |
nipkow |
Hoare logic
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:04:16 +0100 |
clasohm |
new version of HOL/IMP with curried function application
|
file |
diff |
annotate
|