Thu, 10 May 2007 00:39:54 +0200 | wenzelm | tuned argument_type_of; | changeset | files |
Thu, 10 May 2007 00:39:53 +0200 | wenzelm | added destructors from drule.ML; | changeset | files |
Thu, 10 May 2007 00:39:52 +0200 | wenzelm | moved some operations to more_thm.ML and conv.ML; | changeset | files |
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 |