isabelle: Changelog

urbanc [Sun, 27 Nov 2005 04:59:20 +0100] rev 18263

cleaned up all examples so that they work with the current nominal-setting.

urbanc [Sun, 27 Nov 2005 03:55:16 +0100] rev 18262

finished cleaning up the parts that collect lemmas (with instantiations) under some general names

berghofe [Sat, 26 Nov 2005 18:41:41 +0100] rev 18261

Corrected treatment of non-recursive abstraction types.

wenzelm [Fri, 25 Nov 2005 21:14:34 +0100] rev 18260

tuned induct proofs;

wenzelm [Fri, 25 Nov 2005 20:57:51 +0100] rev 18259

induct: insert defs in object-logic form; export guess_instance;

wenzelm [Fri, 25 Nov 2005 19:20:56 +0100] rev 18258

tuned induct proofs;

wenzelm [Fri, 25 Nov 2005 19:09:44 +0100] rev 18257

tuned induct proofs;

wenzelm [Fri, 25 Nov 2005 18:58:43 +0100] rev 18256

consume: unfold defs in all major prems;

wenzelm [Fri, 25 Nov 2005 18:58:42 +0100] rev 18255

revert_skolem: fall back on Syntax.deskolem;

wenzelm [Fri, 25 Nov 2005 18:58:41 +0100] rev 18254

forall_conv ~1;

isabelle