wenzelm [Thu, 13 Apr 2000 15:00:42 +0200] rev 8699
intro/elim_tac: match only;
nipkow [Thu, 13 Apr 2000 10:30:28 +0200] rev 8698
made mod_less_divisor a simplification rule.
wenzelm [Wed, 12 Apr 2000 23:52:50 +0200] rev 8697
InductMethod.concls_of;
wenzelm [Wed, 12 Apr 2000 23:52:21 +0200] rev 8696
tuned;
wenzelm [Wed, 12 Apr 2000 23:51:57 +0200] rev 8695
export concl_of;
induct method: admit "_";
wenzelm [Wed, 12 Apr 2000 23:49:10 +0200] rev 8694
tuned \isasymlbrace;
wenzelm [Wed, 12 Apr 2000 23:47:47 +0200] rev 8693
'insts' syntax;
'insert' method;
wenzelm [Wed, 12 Apr 2000 23:46:06 +0200] rev 8692
improved 'induct(_tac)' syntax;
wenzelm [Wed, 12 Apr 2000 23:45:21 +0200] rev 8691
added 'insert' method;
wenzelm [Wed, 12 Apr 2000 23:45:01 +0200] rev 8690
added inst, insts;