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;
wenzelm [Thu, 05 Jul 2007 20:01:28 +0200] rev 23591
simplified ObjectLogic.atomize;
wenzelm [Thu, 05 Jul 2007 20:01:26 +0200] rev 23590
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;