Jan van Brügge (Mar 10 2022 at 13:23): Jan van Brügge (Mar 10 2022 at 13:23):Is there a tactic that works like resolve_tac, but only does the unification and not solve the goal yet? The rule I want to resolve with has variables in the assumptions that are not part of the conclusion and I want to instantiate them with id. To do that I would first need to fix all variables that are used in the goal (i.e. do unification). If I don't do this I end up with a goal like prems ==> bij (?f3 <all forall bound variables>) which isabelle refuses to unify with id if i try to apply bij_id
Last updated: Jul 15 2022 at 23:21 UTC