Email Gateway (Aug 18 2022 at 12:00): Email Gateway (Aug 18 2022 at 12:00):From: John Matthews <matthews@galois.com>
Hello,
In starting to switch my theories over to Isabelle2008, I ran into an
unexpected behavior of the "find theorems" command: It can't find any
theorems matching just "pred", but finds lots of theorems matching
"Int.pred".
Is this because the constant "pred" has been hidden? If so, is there a
way to have the find theorems command include hidden constants too?
Thanks,
-john
Email Gateway (Aug 18 2022 at 12:01):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear John,
Is this because the constant "pred" has been hidden? If so, is there a
way to have the find theorems command include hidden constants too?
Indeed, "pred" has been hidden since (at least) Isablle2007 (although
there it was named Numeral.pred, not Int.pred).
Generally, to "hide" constant means nothing else than dropping the
unqualified name access. So, the string "pred" does not refer to this
constant. This rules out find_theorems as a device to search for
"hidden" constants.
Florian
florian_haftmann.vcf
signature.asc
Last updated: May 03 2024 at 08:18 UTC