[isabelle-dev] bnf_decl axiomatization

[Jasmin Blanchette]

Am 13.05.2014 um 15:35 schrieb Makarius <makarius at sketis.net>:

> On Tue, 13 May 2014, Dmitriy Traytel wrote:
> 
>> 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".
> 
> Odd.  We basically have this hierarchy of danger:

The name "bnf_decl" was not trying to encode any level of danger. It was just trying to say what the command does. And what it does is to introduce an "opaque BNF", just like "typedecl" introduces an "opaque type". (I'm using "opaque" in the sense: without structure, unconstrained, uninterpreted, ...) But whereas "typedecl" works with danger level 0 because types are a built-in concept of HOL, for "bnf_decl" we needed axioms -- and I agree in retrospect that a clear indication of the higher danger level is more important information than the symmetry with "typedecl".

Jasmin