Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] [isabelle] Suggestions for src/HOL/Fun.thy

view this post on Zulip Email Gateway (Oct 10 2022 at 10:29):

From: Lawrence Paulson <>
The new proposed lemmas look useful but a little arbitrary. For example, one can imagine multiplicative versions of most of them as equally justifiable and useful.

It makes sense to remove needless restrictions from material we already have and then to fill any obvious gaps in the material, but we do need a way of stopping.

Tobias’s suggestion of a new theory is helpful especially if it arrives later in the build process. Note that presburger is not actually available in Fun.thy.


isabelle-dev mailing list

Last updated: Feb 24 2024 at 04:17 UTC