src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
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