| 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 |
| Mon, 03 May 2010 16:26:47 +0200 | wenzelm | minor tuning of Thm.strip_shyps -- no longer pervasive; | changeset | files |
| Mon, 03 May 2010 15:34:55 +0200 | wenzelm | simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here; | changeset | files |
| Mon, 03 May 2010 14:38:18 +0200 | wenzelm | old NEWS on global operations; | changeset | files |
| Mon, 03 May 2010 14:31:33 +0200 | wenzelm | ProofContext.init_global; | changeset | files |
| Mon, 03 May 2010 14:25:56 +0200 | wenzelm | renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing; | changeset | files |