Email Gateway (Aug 13 2025 at 07:42): Email Gateway (Aug 13 2025 at 07:42):From: Peter <cl-isabelle-users@lists.cam.ac.uk>
Hi List,
I'm importing a theory from AFP, and this defines some syntax via
abbreviations:
abbreviation LCons_abbr (infixr ‹$› 65) where "x $ xs ≡ LCons x xs"
is there a way to get rid of that syntax (and the abbreviation)?
I can do
no_notation LCons_abbr (infixr ‹$› 65)
but that will keep the abbreviation, and display LCons as LCons_abbrv. A
hide_const LCons_abbrv
also does not have the desired effect, displaying LCons as
"??.LazyList_Operations.LCons_abbr a b"
--
Peter
Last updated: Aug 20 2025 at 20:23 UTC