Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] case_names, obtains (par_name), and named loca...

Email Gateway (Aug 22 2022 at 10:42):

From: Makarius <makarius@sketis.net>
The cases method never changes the conclusion, so it is just ?thesis.

The extra features of the "induct" family have brought it to the brink of
self-destruction. It is hard to say today what it does and what not. It
needs a major reform.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC