[isabelle] inductive_cases and simplifier

Hi all,

I use the inductive_cases command to deal with rule
inversion. Unfortunately, inductive_cases applies simplification to
the premises of the rule generated. Is there a way to turn this
behavior off?


Stefan Wehr
Programming Languages Group
Department of Computer Science, University of Freiburg
Georges-Köhler-Allee 079, 79110 Freiburg i. Br., Germany
Phone: +49 761 203 8060, Fax: +49 761 203 8052
Room: 00-013, building 079
PGP: Key available from keyserver wwwkeys.de.pgp.net, ID 0x0B9F5CE4

Attachment: pgp7dPOZGjlCZ.pgp
Description: PGP signature

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