Forwarding this error report to the right mailing list ...
--- Begin Message ---
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!
--
Peter
--- End Message ---
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
