| Tue, 09 Oct 2012 22:24:24 +0200 | wenzelm | removed redundant lemma, cf. class zero_neq_one in HOL/Rings.thy; | changeset | files |
| Tue, 09 Oct 2012 21:33:12 +0200 | wenzelm | clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts; | changeset | files |
| Tue, 09 Oct 2012 20:23:58 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 09 Oct 2012 20:05:17 +0200 | wenzelm | clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional; | changeset | files |
| Tue, 09 Oct 2012 19:24:19 +0200 | wenzelm | more explicit flags for facts table; | changeset | files |
| Tue, 09 Oct 2012 15:31:45 +0200 | wenzelm | minor tuning; | changeset | files |