urbanc [Sun, 27 Nov 2005 05:00:43 +0100] rev 18264
added the version of nominal.thy that contains
all properties about support of finite sets
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;