From: Andrea Berlingieri Date: Mon, 17 Jun 2019 08:10:31 +0000 (+0200) Subject: Make 'that is equivalent to' a standalone tactic X-Git-Tag: make_still_working~229^2~1^2~1^2~2 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b8a04566e67338e7e5375ff4175277704cd16432;hp=b8a04566e67338e7e5375ff4175277704cd16432;p=helm.git Make 'that is equivalent to' a standalone tactic Simplify AST types, parsing rules and pp of tactics that had 'that is equivalent to' or 'or equivalently' Modify grafiteEngine accordingly Simplify the signature and the code of the implementations of tactics that had 'that is equivalent to' or 'or equivalently' A new "volatile_hypo" key is added to the parameter list of the currest stack level to indicate that the beta rewriting should happen on that hypothesis, instead of the thesis Modify beta_rewrite accordingly Add some "obvious" terms to the given candidates for the automation (such as refl, sym_eq, trans_eq, etc.) The weakening of the automation is now only partial: the second flag for weakening is off. Setting it on makes theorem proving pretty impossible with the declarative fragment. ---