| Tue, 07 May 2002 14:27:07 +0200 |
wenzelm |
\documentclass{report};
|
changeset |
files
|
| Tue, 07 May 2002 14:26:32 +0200 |
wenzelm |
use eq_thm_prop instead of slightly inadequate eq_thm;
|
changeset |
files
|
| Tue, 07 May 2002 14:24:30 +0200 |
wenzelm |
clarified eq_thm;
|
changeset |
files
|
| Mon, 06 May 2002 09:42:20 +0200 |
nipkow |
Added insert_disjoint and disjoint_insert [simp], and simplified proofs
|
changeset |
files
|
| Sat, 04 May 2002 15:47:21 +0200 |
berghofe |
Added skeletons to speed up rewriting on proof terms.
|
changeset |
files
|
| Tue, 30 Apr 2002 13:00:29 +0200 |
kleing |
tuned
|
changeset |
files
|
| Tue, 30 Apr 2002 12:15:48 +0200 |
kleing |
physical location of isabelle repository is now sunbroy2
|
changeset |
files
|
| Mon, 29 Apr 2002 16:45:12 +0200 |
prensani |
added abstract;corrected RG_Basic Hoare rule.
|
changeset |
files
|
| Mon, 29 Apr 2002 11:30:15 +0200 |
nipkow |
Better compiler proof
|
changeset |
files
|
| Mon, 29 Apr 2002 11:29:54 +0200 |
nipkow |
Had to update proof for some strange reason
|
changeset |
files
|
| Mon, 29 Apr 2002 11:29:34 +0200 |
nipkow |
added rev_take and rev_drop
|
changeset |
files
|
| Fri, 26 Apr 2002 11:47:01 +0200 |
nipkow |
New machine architecture and other direction of compiler proof.
|
changeset |
files
|
| Thu, 25 Apr 2002 17:36:29 +0200 |
nipkow |
added "m <= n ==> m-n = 0" [simp]
|
changeset |
files
|
| Fri, 19 Apr 2002 14:51:33 +0200 |
berghofe |
code generator: wfrec combinator is now implemented by ML function wf_rec.
|
changeset |
files
|