| Tue, 10 Nov 2009 15:32:43 +0100 | wenzelm | define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration; | changeset | files |
| Tue, 10 Nov 2009 14:38:39 +0100 | wenzelm | bang_facts: legacy feature; | changeset | files |
| Tue, 10 Nov 2009 14:38:06 +0100 | wenzelm | tuned proofs; | changeset | files |
| Tue, 10 Nov 2009 13:59:37 +0100 | wenzelm | removed obsolete name_of -- cf. decode; | changeset | files |
| Tue, 10 Nov 2009 13:45:11 +0100 | wenzelm | desymbolize: use Symbol.decode directly; | changeset | files |
| Tue, 10 Nov 2009 13:17:50 +0100 | wenzelm | try SAT_Examples last, to minimize impact of global side-effects; | changeset | files |
| Tue, 10 Nov 2009 13:05:35 +0100 | wenzelm | home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $); | changeset | files |