src/HOL/Codatatype/Tools/bnf_wrap.ML
2012-09-04 blanchet 2012-09-04 renamed theorem
2012-09-04 blanchet 2012-09-04 tuned TODO comment
2012-09-04 blanchet 2012-09-04 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
2012-09-04 blanchet 2012-09-04 allow "*" to indicate no discriminator
2012-09-04 blanchet 2012-09-04 tuned TODOs
2012-09-04 blanchet 2012-09-04 export "wrap" function
2012-09-03 blanchet 2012-09-03 rearrange dependencies
2012-09-03 blanchet 2012-09-03 renamed three BNF/(co)datatype-related commands