wenzelm [Thu, 28 Jul 2005 15:20:00 +0200] rev 16943
added add_tfreesT, add_tfrees;
added bound;
added zero_var_indexesT, zero_var_indexes, zero_var_indexes_subst;
removed add_term_constsT;
tuned;
wenzelm [Thu, 28 Jul 2005 15:19:59 +0200] rev 16942
norm_hhf_rule: Thm.adjust_maxidx_thm before Drule.gen_all;
removed prove_standard, prove_multi_standard;
wenzelm [Thu, 28 Jul 2005 15:19:58 +0200] rev 16941
added add_const_constraint(_i), const_constraint;
added typ_match, typ_unify;
wenzelm [Thu, 28 Jul 2005 15:19:57 +0200] rev 16940
adapted Type.typ_match;
tuned;
wenzelm [Thu, 28 Jul 2005 15:19:56 +0200] rev 16939
Sign.typ_unify;
Term.bound;
tuned rewrite_term;
wenzelm [Thu, 28 Jul 2005 15:19:55 +0200] rev 16938
Term.bound;
wenzelm [Thu, 28 Jul 2005 15:19:54 +0200] rev 16937
print_theory: const constraints;
wenzelm [Thu, 28 Jul 2005 15:19:53 +0200] rev 16936
Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;
wenzelm [Thu, 28 Jul 2005 15:19:51 +0200] rev 16935
Sign.typ_match;
wenzelm [Thu, 28 Jul 2005 15:19:49 +0200] rev 16934
Sign.typ_unify;