Re: [isabelle] Isabelle2016-RC0 - using goal_cases correctly
On Sun, 3 Jan 2016, C. Diekmann wrote:
In Isabelle 2016, I can write:
apply (rule Y)
Or I could write
proof(rule Y, goal_cases)
Is there a nicer way to combine the rule and goal_cases method? Is
this the intended usage?
Yes, the second form is the intended usage. Method "goal_cases" bypasses
the "using" facts, so the comma is always right.
Since the preceeding proof method in this example is just "rule", it might
be also possible to say:
proof (cases rule: Y)
Details depend on the shape of Y.
This archive was generated by a fusion of
Pipermail (Mailman edition) and