| Thu, 22 Apr 1999 13:03:10 +0200 | wenzelm | rep_datatype syntax: 'induction' instead of 'induct'; | changeset | files |
| Thu, 22 Apr 1999 12:50:39 +0200 | wenzelm | add_recdef: actual simpset; | changeset | files |
| Thu, 22 Apr 1999 12:49:34 +0200 | wenzelm | recdef adapted to RecdefPackage.add_recdef; | changeset | files |
| Thu, 22 Apr 1999 12:49:00 +0200 | wenzelm | Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML; | changeset | files |
| Thu, 22 Apr 1999 12:47:13 +0200 | mueller | added ex and Modelcheck | changeset | files |
| Thu, 22 Apr 1999 12:47:07 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 22 Apr 1999 12:42:14 +0200 | mueller | added for mucke translation; | changeset | files |
| Thu, 22 Apr 1999 12:40:11 +0200 | mueller | deleted some old examples in Modelcheck; | changeset | files |