src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
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 register coinductive type's coinduct rule
2013-04-25 blanchet 2013-04-25 generate proper attributes for coinduction rules
2013-04-25 blanchet 2013-04-25 simplified code -- no need for two attempts, the error we get from mixfix the first time is good (and better to get than a parse error in the specification because the user tries to use a mixfix that silently failed)
2013-04-24 blanchet 2013-04-24 proper error generated for wrong mixfix
2013-04-24 blanchet 2013-04-24 honor user-specified name for relator + generalize syntax
2013-04-24 blanchet 2013-04-24 renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
2013-04-24 blanchet 2013-04-24 honor user-specified name for map function
2013-04-24 blanchet 2013-04-24 honor user-specified set function names
2013-04-24 blanchet 2013-04-24 parse set function name
2013-04-23 blanchet 2013-04-23 avoid accidental specialization of the types in the "map" property of codatatypes
2013-04-23 blanchet 2013-04-23 simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)
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-22 traytel 2012-11-22 made SML/NJ happier
2012-10-03 blanchet 2012-10-03 thread the right local theory through + reenable parallel proofs for previously problematic theories
2012-10-02 blanchet 2012-10-02 continued changing type of corec type
2012-10-02 blanchet 2012-10-02 removed dead params and dead code
2012-10-02 blanchet 2012-10-02 changed type of corecursor for the nested recursion case
2012-10-01 blanchet 2012-10-01 fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)
2012-10-01 blanchet 2012-10-01 tweaked corecursor/coiterator tactic
2012-10-01 blanchet 2012-10-01 changed the type of the recursor for nested recursion
2012-09-28 blanchet 2012-09-28 renamed ML file in preparation for next step