src/HOL/Codatatype/Tools/bnf_sugar.ML
Thu, 30 Aug 2012 11:31:47 +0200 blanchet added discriminator theorems
Thu, 30 Aug 2012 09:48:27 +0200 blanchet more work on sugar
Thu, 30 Aug 2012 09:47:46 +0200 blanchet changed order of arguments to "bnf_sugar"
Thu, 30 Aug 2012 09:47:46 +0200 blanchet define selectors and discriminators
Thu, 30 Aug 2012 09:47:46 +0200 blanchet more work on BNF sugar -- up to derivation of nchotomy
Thu, 30 Aug 2012 09:47:46 +0200 blanchet more work on BNF sugar
Thu, 30 Aug 2012 09:47:46 +0200 blanchet started work on datatype sugar
less more (0) tip