src/HOL/Library/bnf_axiomatization.ML
2015-09-23 wenzelm 2015-09-23 tuned signature;
2015-09-22 wenzelm 2015-09-22 HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;
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