src/HOL/BNF/Tools/bnf_wrap.ML
2013-04-26 blanchet 2013-04-26 more intuitive syntax for equality-style discriminators of nullary constructors
2013-04-26 blanchet 2013-04-26 changed discriminator default: avoid mixing ctor and dtor views
2013-04-25 blanchet 2013-04-25 renamed "wrap_data" to "wrap_free_constructors"
2013-04-25 blanchet 2013-04-25 generate proper attributes for coinduction rules
2013-04-25 blanchet 2013-04-25 start making "wrap_data" more robust
2013-04-25 blanchet 2013-04-25 no eta-expansion for case in split rules and case_conv
2013-04-24 blanchet 2013-04-24 apply arguments to f and g in "case_cong"
2013-04-24 blanchet 2013-04-24 eta-contracted weak congruence rules (like in the old package)
2013-04-24 blanchet 2013-04-24 honor user-specified set function names
2013-04-23 blanchet 2013-04-23 tuning
2013-04-23 blanchet 2013-04-23 fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-11 traytel 2013-04-11 do not add case translation syntax in rep_datatype compatibility mode
2013-04-11 traytel 2013-04-11 run type inference on input to wrap_data
2013-04-11 traytel 2013-04-11 installed case translations in BNF package
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2013-03-08 blanchet 2013-03-08 proper type inference for default values
2012-11-26 wenzelm 2012-11-26 tuned command descriptions;
2012-10-03 blanchet 2012-10-03 made code more conform to rest of BNF package
2012-09-30 blanchet 2012-09-30 tuning
2012-09-30 traytel 2012-09-30 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
2012-09-28 blanchet 2012-09-28 compatibility option to use "rep_datatype"
2012-09-27 blanchet 2012-09-27 use a nicer scheme to indexify names
2012-09-27 blanchet 2012-09-27 repaired signature
2012-09-27 blanchet 2012-09-27 lower the defaults for the number of bits, based on an example by Lukas Bulwahn
2012-09-26 blanchet 2012-09-26 tweaked theorem names (in particular, dropped s's)
2012-09-26 blanchet 2012-09-26 generate high-level "coinduct" and "strong_coinduct" properties
2012-09-26 blanchet 2012-09-26 parameterized "subst_tac"
2012-09-26 blanchet 2012-09-26 generate high-level "maps", "sets", and "rels" properties
2012-09-23 blanchet 2012-09-23 started work on generation of "rel" theorems
2012-09-21 blanchet 2012-09-21 renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"