src/HOL/Codatatype/Tools/bnf_sugar.ML
2012-08-30 blanchet 2012-08-30 generate "disc_exhaust" property
2012-08-30 blanchet 2012-08-30 generate "disc_distinct" theorems
2012-08-30 blanchet 2012-08-30 added discriminator theorems
2012-08-30 blanchet 2012-08-30 more work on sugar
2012-08-30 blanchet 2012-08-30 changed order of arguments to "bnf_sugar"
2012-08-30 blanchet 2012-08-30 define selectors and discriminators
2012-08-30 blanchet 2012-08-30 more work on BNF sugar -- up to derivation of nchotomy
2012-08-30 blanchet 2012-08-30 more work on BNF sugar
2012-08-30 blanchet 2012-08-30 started work on datatype sugar