wenzelm [Mon, 19 Nov 2001 20:47:39 +0100] rev 12242
multi_theorem: common statement header (covers *all* results);
wenzelm [Mon, 19 Nov 2001 20:46:38 +0100] rev 12241
fixed comment;
goal: unbind if multiple statements;
wenzelm [Mon, 19 Nov 2001 20:46:05 +0100] rev 12240
induct method: localize rews for rule;
berghofe [Mon, 19 Nov 2001 17:42:00 +0100] rev 12239
Now handles different theorems with same name more gracefully.
berghofe [Mon, 19 Nov 2001 17:40:45 +0100] rev 12238
Improved error message.
berghofe [Mon, 19 Nov 2001 17:40:07 +0100] rev 12237
Added setup.
berghofe [Mon, 19 Nov 2001 17:39:31 +0100] rev 12236
Moved fastype to Envir.
berghofe [Mon, 19 Nov 2001 17:38:09 +0100] rev 12235
Further restructuring of theorem naming functions.
berghofe [Mon, 19 Nov 2001 17:36:40 +0100] rev 12234
Added setup for proof rewrite rules.
berghofe [Mon, 19 Nov 2001 17:36:05 +0100] rev 12233
- Fixed bug in shrink
- Restored old behaviour of thm_proof
- Eliminated reference from theory data