2007-10-20 | wenzelm | tuned; | changeset | files |
2007-10-20 | wenzelm | add_inductive: more careful handling of abbrevs -- do not expand prematurely; | changeset | files |
2007-10-20 | wenzelm | fixed proof: neq0_conv; | changeset | files |
2007-10-20 | chaieb | fixed proofs | changeset | files |
2007-10-20 | chaieb | neq0_conv removed from [iff] -- causes problems by simple goals with blast, auto etc... | changeset | files |
2007-10-19 | wenzelm | export_code: proper command; | changeset | files |
2007-10-19 | wenzelm | warn_open: context position; | changeset | files |
2007-10-19 | wenzelm | sorry: proper command; | changeset | files |
2007-10-19 | wenzelm | tuned proofs: avoid implicit prems; | changeset | files |
2007-10-19 | wenzelm | tuned proofs; | changeset | files |
2007-10-19 | wenzelm | internal tuning: class_target, fork_mixfix, declare_const (singleton), abbrev; | changeset | files |
2007-10-19 | wenzelm | tuned interfaces; | changeset | files |
Loading... |