Email Gateway (Aug 19 2022 at 11:47): Email Gateway (Aug 19 2022 at 11:47):From: Peter Lammich <lammich@in.tum.de>
Referring to Isabelle_12-Sep-2013:
When using overloading from Monad_Syntax, abbreviations are no longer
displayed in output syntax:
theory Scratch
imports
Main
"~~/src/HOL/Library/Monad_Syntax"
begin
abbreviation "my_abbrev \<equiv> [True]"
term "foo (Some my_abbrev) f" (* Yields: foo (Some my_abbrev) f *)
term "bind (Some my_abbrev) f" (* Yields: Some [True] >>= f*)
Note that the abbreviation is not displayed in the second term.
Can I somehow get my abbreviations back?
Note that this is a VERY ANNOYING behaviour, as it renders the output
almost unreadable for larger terms!
Last updated: Apr 25 2024 at 08:20 UTC