Email Gateway (Apr 22 2025 at 17:38): Email Gateway (Apr 22 2025 at 17:38):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Hi Gerwin,
When grooming old mail threads I stumbled over this.
Did you have a change to try this out?
Florian
Am 26.07.24 um 01:15 schrieb Gerwin Klein (via cl-isabelle-users Mailing
List):
Thanks, I'll give that a shot.
Cheers,
GerwinOn 26 Jul 2024, at 02:29, Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de> wrote:
There are 146 occurrences of the string "shiftl1" in l4v outside the word library (similar order of magnitude for shiftr1). It’s likely that most of these are harmless (a lot look like they refer to the lemma "shiftr_shiftl1", which does not actually refer to the constant shiftl1), but I don’t particularly feel like spending a lot of time going through all of them manually for no pressing reason.
I’d be happy to try out if adding the legacy alias theory works, but if it doesn’t I would not want this change unless somebody fixes the proofs.
My proposal: I’ll send a minimal patch based on AFP 2024 containing the transition from logical constants to abbreviations and then let’s see what effects occur and what to conlude from that.Find attached a minimal patch as basis for a test run.
Cheers,
Florian
<abbrev.txt><OpenPGP_0xA707172232CFA4E9.asc>
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Last updated: May 06 2025 at 08:28 UTC