[isabelle] disabling datatype syntax
Is there a way to temporarily enable/disable syntax declared on
datatype constructors? I assume it would be done with no_syntax or
no_translations, but I'm not sure how.
I just tried a no_translations declaration, and that didn't seem to
work. I'm not sure what the no_syntax declaration would look like. The
only line that appears relevant from running isar-help-syntax is
logic = "!(" logic => "Start" (80)
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)
This archive was generated by a fusion of
Pipermail (Mailman edition) and