Am 12.05.2014 um 23:10 schrieb Makarius <makar...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
