wenzelm [Thu, 05 Jul 2007 20:01:38 +0200] rev 23601
added type conv;
merge_thys: removed dead exception handlers;
tuned;
wenzelm [Thu, 05 Jul 2007 20:01:37 +0200] rev 23600
removed comments -- no exception TERM;
merge_list: exception THEORY;
wenzelm [Thu, 05 Jul 2007 20:01:36 +0200] rev 23599
added is_reflexive;
wenzelm [Thu, 05 Jul 2007 20:01:35 +0200] rev 23598
tuned;
wenzelm [Thu, 05 Jul 2007 20:01:34 +0200] rev 23597
simplified has_meta_prems;
wenzelm [Thu, 05 Jul 2007 20:01:33 +0200] rev 23596
moved type conv to thm.ML;
renamed Conv.is_refl to Thm.is_reflexive;
misc tuning of basic conversions;
wenzelm [Thu, 05 Jul 2007 20:01:32 +0200] rev 23595
the_theory/proof: error instead of exception Fail;
wenzelm [Thu, 05 Jul 2007 20:01:31 +0200] rev 23594
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
added flat_rule filter for addXXs etc.;
wenzelm [Thu, 05 Jul 2007 20:01:30 +0200] rev 23593
renamed Conv.is_refl to Thm.is_reflexive;
wenzelm [Thu, 05 Jul 2007 20:01:29 +0200] rev 23592
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
simplified ObjectLogic.atomize;