[isabelle-dev] bnf_decl axiomatization

Jasmin Blanchette jasmin.blanchette at gmail.com
Tue May 13 15:44:06 CEST 2014

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".


More information about the isabelle-dev mailing list