Update: I found it seems actaully easy to implement an attribute by
src/Isar/isar_cmd.ML. I guess the problem could be solved quickly and apologize for the interruption.
Could a translation rule be disabled by an option like
Actually, I have a translation rule to conceal complicated detail that is not intended to be displayed to users, like this:
datatype 'a complicated = Complicated 'a syntax omitted :: logic translations "omitted" <= "CONST Complicated x" term "Complicated x" (* displays "omitted :: 'a complicated" *)
Then I wish some way for my users, ideally an option, to disable this rule in order to have a look at the omitted detail.
I know the command
no_translation, but I think it's not friendly for users, since, as far as I know, it requires giving the complete expression of the rule
no_translations "omitted" <= "CONST Complicated detail" term "Complicated x" (* displays "Complicated x :: 'a complicated" *)
I really wish something like an option
declare[[some_option_to_show_omitted_detail = true]]
Any suggestions about this?
Last updated: Sep 25 2021 at 09:17 UTC