| Thu, 22 Apr 1999 13:16:22 +0200 | wenzelm | switch_theory: Context.pass; | changeset | files |
| Thu, 22 Apr 1999 13:04:50 +0200 | wenzelm | recdef (TFL) now requires theory Recdef; | changeset | files |
| Thu, 22 Apr 1999 13:04:23 +0200 | wenzelm | recdef requires theory Recdef; | changeset | files |
| Thu, 22 Apr 1999 13:03:46 +0200 | wenzelm | tuned; | changeset | files |
| 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 |