| Mon, 22 Mar 2010 00:51:18 +0100 | wenzelm | replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom; | changeset | files |
| Mon, 22 Mar 2010 00:48:56 +0100 | wenzelm | replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless; | changeset | files |
| Sun, 21 Mar 2010 22:24:04 +0100 | wenzelm | add_axiom: axiomatize "unconstrained" version, with explicit of_class premises; | changeset | files |
| Sun, 21 Mar 2010 22:13:31 +0100 | wenzelm | Logic.mk_of_sort convenience; | changeset | files |
| Sun, 21 Mar 2010 19:30:19 +0100 | wenzelm | more explicit invented name; | changeset | files |
| Sun, 21 Mar 2010 19:28:25 +0100 | wenzelm | minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization'; | changeset | files |