src/HOL/Codatatype/Tools/bnf_comp.ML
2012-09-09 traytel 2012-09-09 full name of a type as key in bnf table
2012-09-09 traytel 2012-09-09 open typedefs everywhere in the package
2012-09-06 traytel 2012-09-06 handle type constructors not known to be a BNF using the DEADID BNF
2012-09-06 traytel 2012-09-06 respect order of/additional type variables supplied by the user in fixed point constructions;
2012-09-05 traytel 2012-09-05 do not trivialize important internal theorem in quick_and_dirty mode
2012-09-04 blanchet 2012-09-04 more work on sugar + simplify Trueprop + eq idiom everywhere
2012-09-04 blanchet 2012-09-04 more work on FP sugar
2012-09-04 traytel 2012-09-04 no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
2012-08-30 blanchet 2012-08-30 more work on BNF sugar
2012-08-30 blanchet 2012-08-30 renamed ML function for consistency
2012-08-30 blanchet 2012-08-30 killed obsolete "bnf_of_typ" command
2012-08-30 blanchet 2012-08-30 removed dead code
2012-08-30 blanchet 2012-08-30 have "bnf_of_typ" command seal the BNF
2012-08-28 blanchet 2012-08-28 added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)