2001-11-19 wenzelm improved treatment of common result name;
2001-11-19 wenzelm tuned;
2001-11-19 wenzelm multi_theorem: common statement header (covers *all* results);
2001-11-19 wenzelm fixed comment;
2001-11-19 wenzelm induct method: localize rews for rule;
2001-11-19 berghofe Now handles different theorems with same name more gracefully.
2001-11-19 berghofe Improved error message.
2001-11-19 berghofe Added setup.
2001-11-19 berghofe Moved fastype to Envir.
2001-11-19 berghofe Further restructuring of theorem naming functions.
2001-11-19 berghofe Added setup for proof rewrite rules.
2001-11-19 berghofe - Fixed bug in shrink
2001-11-19 berghofe Replaced devar by Envir.head_norm
2001-11-19 berghofe Moved head_norm and fastype from unify.ML to envir.ML
Loading...
(0) -10000 -3000 -1000 -300 -100 -14 +14 +100 +300 +1000 +3000 +10000 +30000 tip