Stream: Beginner Questions

Topic: rule/assumption that do not unify schematic variables

view this post on Zulip Jan van Brügge (Nov 15 2023 at 18:44):

Is there an equivalent to apply assumption and apply (rule ...) that do not unify schematic variables? I know in ML there exist eq_assume_tac and match_tac but is there an isabelle equivalent? Currently I use apply (tactic ...) as a workaround

view this post on Zulip Kevin Kappelmann (Nov 15 2023 at 20:18):

Is the AFP an option for you or are you looking for something in the standard distribution?

view this post on Zulip Jan van Brügge (Nov 15 2023 at 20:59):

rather the latter, i mean the workaround does work

view this post on Zulip Kevin Kappelmann (Nov 15 2023 at 21:18):

Then there's no alternative as far as I know. In the AFP, there are assumption and rule methods with adjustable unification algortihms:

https://www.isa-afp.org/sessions/ml_unification/#Unify_Resolve_Tactics

Last updated: Oct 28 2025 at 16:29 UTC