Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] inductive_cases and simplifier

Email Gateway (Aug 18 2022 at 12:07):

From: Stefan Wehr <wehr@informatik.uni-freiburg.de>
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?

Cheers,
Stefan

Last updated: Sep 08 2025 at 16:25 UTC