| Thu, 10 May 2007 00:39:51 +0200 | wenzelm | Conversions: primitive equality reasoning (from drule.ML); | changeset | files |
| Thu, 10 May 2007 00:39:50 +0200 | wenzelm | added conv.ML; | changeset | files |
| Thu, 10 May 2007 00:39:49 +0200 | wenzelm | Thm.match; | changeset | files |
| Thu, 10 May 2007 00:39:48 +0200 | wenzelm | moved some Drule operations to Thm (see more_thm.ML); | changeset | files |
| Thu, 10 May 2007 00:39:46 +0200 | wenzelm | Thm.first_order_match; | changeset | files |
| Thu, 10 May 2007 00:39:45 +0200 | wenzelm | moved conversions to structure Conv; | changeset | files |
| Wed, 09 May 2007 23:28:18 +0200 | krauss | "fun" command: Changed pattern compatibility proof back from "simp_all" to the slower but more robust "auto" | changeset | files |