Re: [isabelle] Illegal schematic variable(s) in case
> proof(induction taking: foo rule: ienv_relatedE)
> case none
thanks for the hint, this works nicely.
> proof(rule ienv_relatedE)
> assume "nenv foo = None" "penv foo = None"
> is debatable, as induction is normally a much stronger proof principle
> than case analysis.
It probably incites more head-scratching from readers of the proof as to
why exactly induction is used there.
> Alternatively, you can see whether the cases method
> can be easily extended with "taking".
I will keep this in mind for later when I'm done with my current
This archive was generated by a fusion of
Pipermail (Mailman edition) and