Re: [isabelle] Isabelle2016-RC0 - using goal_cases correctly



On Sun, 3 Jan 2016, C. Diekmann wrote:

In Isabelle 2016, I can write:

lemma "X"
 apply (rule Y)
 proof(goal_cases)
   case 1

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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.