src/HOL/Library/bnf_axiomatization.ML
2015-09-04 wenzelm 2015-09-04 close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2014-10-30 wenzelm 2014-10-30 proper syntax categery "name" -- as usual and as documented;
2014-10-13 wenzelm 2014-10-13 Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
2014-09-05 blanchet 2014-09-05 added 'plugins' option to control which hooks are enabled
2014-09-05 blanchet 2014-09-05 introduced mechanism to filter interpretations
2014-06-10 blanchet 2014-06-10 changed syntax of map: and rel: arguments to BNF-based datatypes
2014-05-26 blanchet 2014-05-26 got rid of '=:' squiggly
2014-05-13 traytel 2014-05-13 bnf_decl -> bnf_axiomatization