Mon, 05 Jun 2006 21:54:25 +0200 | wenzelm | guess: more careful about local polymorphism; | changeset | files |
Mon, 05 Jun 2006 21:54:24 +0200 | wenzelm | assm_tac: try rule termI; | changeset | files |
Mon, 05 Jun 2006 21:54:23 +0200 | wenzelm | added params_of, prems_of; | changeset | files |
Mon, 05 Jun 2006 21:54:22 +0200 | wenzelm | added matches_seq (left-to-right matching, intermediate beta-normalization); | changeset | files |
Mon, 05 Jun 2006 21:54:21 +0200 | wenzelm | support embedded terms; | changeset | files |
Mon, 05 Jun 2006 21:54:20 +0200 | wenzelm | allow non-trivial schematic goals (via embedded term vars); | changeset | files |
Mon, 05 Jun 2006 19:54:12 +0200 | krauss | HOL/Tools/fundef_package: Cleanup | changeset | files |