wenzelm [Tue, 10 Nov 2009 15:33:35 +0100] rev 33552
removed unused Quickcheck_RecFun_Simps;
wenzelm [Tue, 10 Nov 2009 15:32:43 +0100] rev 33551
define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;
wenzelm [Tue, 10 Nov 2009 14:38:39 +0100] rev 33550
bang_facts: legacy feature;
wenzelm [Tue, 10 Nov 2009 14:38:06 +0100] rev 33549
tuned proofs;
wenzelm [Tue, 10 Nov 2009 13:59:37 +0100] rev 33548
removed obsolete name_of -- cf. decode;
wenzelm [Tue, 10 Nov 2009 13:45:11 +0100] rev 33547
desymbolize: use Symbol.decode directly;
recovered coding conventions of this file;
wenzelm [Tue, 10 Nov 2009 13:17:50 +0100] rev 33546
try SAT_Examples last, to minimize impact of global side-effects;
wenzelm [Tue, 10 Nov 2009 13:05:35 +0100] rev 33545
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
paulson [Tue, 10 Nov 2009 09:22:55 +0000] rev 33544
Inserted missing theory dependency
wenzelm [Mon, 09 Nov 2009 21:56:55 +0100] rev 33543
merged