Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle]Simplification beneath foundational terms – pro...


view this post on Zulip Email Gateway (Aug 23 2022 at 08:57):

From: Simon Wimmer <wimmersimon@gmail.com>
Dear Florian,

thanks for your analysis.

I fully agree that the best way would be to generate
the rule automatically but not declare it as a default.

As someone who has run into this problem frequently,
this would allow me to conveniently get around it
without writing a lot of boilerplate code.

Simon


Last updated: Apr 30 2024 at 01:06 UTC