Hi hol-info, Quick question: is there a tactic for instantiating a nested existential based on a name? Example: for a goal such as
?x y z. ... y ... I want to use a tactic foo_tac `y` `5` and get: ?x z. ... 5 ... Is there such a foo_tac tactic? I suspect this functionality is there somewhere already. If not, then I'll implement it. Note: I don't need the advanced feature of being able to instantiate it with `x+z+1` where the variables refer to the other existentially quantified variables. Many thanks, Magnus ------------------------------------------------------------------------------ Transform Data into Opportunity. Accelerate data analysis in your applications with Intel Data Analytics Acceleration Library. Click to learn more. http://pubads.g.doubleclick.net/gampad/clk?id=278785351&iu=/4140 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
