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