[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[0] => "Start" (80)

Chris Capel
-- 
"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 MHonArc.