Email Gateway (Oct 10 2022 at 10:29): Email Gateway (Oct 10 2022 at 10:29):From: Lawrence Paulson <lp15@cam.ac.uk>
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.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 24 2024 at 20:16 UTC