[isabelle-dev] bnf_decl axiomatization

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Tue May 13 08:09:24 CEST 2014

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


More information about the isabelle-dev mailing list