[isabelle-dev] bnf_decl axiomatization

[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. ;)

Jasmin