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: Apr 30 2025 at 08:27 UTC