Re: [isabelle] Remaining Cases in Induction Proofs



Dear Patrick,

> Which brings me to my original point :-D
> 
> I would love to just rewrite the above proof to something like:
> 
> proof (induct v and p and d and r and l)
> case A: … next
> case B: … next
> case C: … next
> remaining_cases by auto
> qed

Then just do it :-)

proof (induct v and p and d and r and l)
  case A: … next
  case B: … next
  case C: … next
qed auto (* solves remaining cases *)

Hope this helps,
René






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