| Wed, 10 Oct 2012 15:21:26 +0200 | wenzelm | more explicit namespace prefix for 'statespace' -- duplicate facts; | changeset | files |
| Wed, 10 Oct 2012 15:17:40 +0200 | wenzelm | eliminated spurious fact duplicates; | changeset | files |
| Wed, 10 Oct 2012 15:01:20 +0200 | wenzelm | modernized dynamic "rules" -- avoid rebinding of static facts; | changeset | files |
| 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 |