[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