| Mon, 03 May 2010 22:00:06 +0200 | wenzelm | UNDISCH/DISJ_CASESL: eliminated slightly odd Thm.legacy_freezeT -- these rules appear to be applied to thms with fixed types only; | changeset | files |
| Mon, 03 May 2010 20:53:49 +0200 | wenzelm | replaced Thm.legacy_freezeT by Thm.unvarify_global -- these facts stem from closed definitions, i.e. there are no term Vars; | changeset | files |
| Mon, 03 May 2010 20:13:36 +0200 | wenzelm | renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze; | changeset | files |