| Fri, 23 Sep 2005 16:05:42 +0200 | nipkow | rules -> iprover | file | diff | annotate |
| Thu, 25 Aug 2005 16:13:09 +0200 | berghofe | Adapted to new code generator syntax. | file | diff | annotate |
| Fri, 17 Jun 2005 16:12:49 +0200 | haftmann | migrated theory headers to new format | file | diff | annotate |
| Thu, 21 Apr 2005 22:02:06 +0200 | wenzelm | superceded by Pure.thy and CPure.thy; | file | diff | annotate |
| Wed, 07 May 2003 16:58:17 +0200 | berghofe | Some tuning: | file | diff | annotate |
| Mon, 28 Apr 2003 10:33:42 +0200 | berghofe | Converted main proofs to Isar. | file | diff | annotate |
| Wed, 13 Nov 2002 15:34:01 +0100 | berghofe | Removed (now unneeded) declarations of realizers for bar induction. | file | diff | annotate |
| Wed, 07 Aug 2002 16:49:25 +0200 | berghofe | Removed (now unneeded) declarations of realizers for induction on lists and letters. | file | diff | annotate |
| Sun, 21 Jul 2002 15:44:42 +0200 | berghofe | Examples for program extraction in HOL. | file | diff | annotate |