| Sun, 15 Nov 2009 21:58:40 +0100 | wenzelm | add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature; | changeset | files |
| Sun, 15 Nov 2009 20:57:42 +0100 | wenzelm | axiomatization: declare Spec_Rules, direct result; | changeset | files |
| Sun, 15 Nov 2009 20:56:34 +0100 | wenzelm | use simultaneous Morphics.fact; | changeset | files |
| Sun, 15 Nov 2009 20:39:22 +0100 | wenzelm | primitive defs: clarified def (axiom name) vs. description; | changeset | files |
| Sun, 15 Nov 2009 19:45:05 +0100 | wenzelm | eliminated obsolete thm position tags; | changeset | files |
| Sun, 15 Nov 2009 19:44:29 +0100 | wenzelm | permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP); | changeset | files |