| 2005-09-23 | nipkow | rules -> iprover | file | diff | annotate |
| 2005-08-25 | berghofe | Adapted to new code generator syntax. | file | diff | annotate |
| 2005-06-17 | haftmann | migrated theory headers to new format | file | diff | annotate |
| 2004-10-13 | nipkow | mod becuase of chnage in induct | file | diff | annotate |
| 2003-04-28 | berghofe | Converted main proof to Isar. | file | diff | annotate |
| 2002-07-21 | berghofe | Examples for program extraction in HOL. | file | diff | annotate |