| Thu, 11 Oct 2007 19:10:24 +0200 | wenzelm | replaced Term.equiv_types by Type.similar_types; | changeset | files |
| Thu, 11 Oct 2007 19:10:23 +0200 | wenzelm | dest/cert_def: replaced Pretty.pp by explicit Proof.context; | changeset | files |
| Thu, 11 Oct 2007 19:10:22 +0200 | wenzelm | added elim_implies (more convenient argument order); | changeset | files |
| Thu, 11 Oct 2007 19:10:21 +0200 | wenzelm | removed obsolete flip; | changeset | files |
| Thu, 11 Oct 2007 19:10:20 +0200 | wenzelm | moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML); | changeset | files |
| Thu, 11 Oct 2007 19:10:19 +0200 | wenzelm | replaced (flip Thm.implies_elim) by Thm.elim_implies; | changeset | files |
| Thu, 11 Oct 2007 19:10:17 +0200 | wenzelm | moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML); | changeset | files |
| Thu, 11 Oct 2007 18:58:34 +0200 | wenzelm | usedir: added HOL_USEDIR_OPTIONS; | changeset | files |