[isabelle-dev] bnf_decl axiomatization

[Dmitriy Traytel]

Am 13.05.2014 08:09, schrieb Jasmin Christian Blanchette:
> Am 12.05.2014 um 23:10 schrieb Makarius <makarius at sketis.net>:
>
>> This sounds both a bit like "testing-unstable-HOL".  But there is no problem to experiment with axiomatizations, if it clear to the user what it is, and not a seamingly harmless "bnf_decl".
> For the record: The name "bnf_decl" was modeled after "typedecl", since they provide similar services. But now that you point it out, I agree that the axiomatic component of "bnf_decl" should be emphasized.
>
>> So why not just call it 'bnf_axiomatization' following the recent naming trend?
> That's a nice name. Dmitriy, let's go for it. ;)

Cf. 5fff4dc31d34.

Let me explain Jasmin's ";)": bnf_axiomatization was the name, I 
intended for the command first, before I was persuaded by my colleagues 
to correlate the name with "typedecl" rather than "axiomatization".

Dmitriy