Re: [isabelle] print_cases shows non-existing schematic variable



> The drop_schematic above drops term bindings that happen to contain
> left-over schematic variables, i.e. have not been properly determined by
> other means (further instantiation by the proof method etc.).

The problem is that the 'cases' method doesn't instantiate the rule
before setting up the cases, as opposed to what 'induct' does. If I write

  proof (cases rule: foo[where ...])

I get the '?case' bindings.

I completely understand why Isar text can't be schematic, which is why
I'm wondering whether the 'cases' method can be changed to perform
matching before setting up the cases.

Cheers
Lars




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