src/HOL/BNF/Tools/ctr_sugar.ML
Tue, 05 Nov 2013 11:17:42 +0100 blanchet make local theory operations non-pervasive (makes more intuitive sense)
Tue, 05 Nov 2013 05:48:08 +0100 blanchet added some N2M caching
Fri, 18 Oct 2013 15:25:39 +0200 blanchet conceal more ugly constructions
Fri, 18 Oct 2013 14:58:02 +0200 blanchet set code attribute on discriminator equations
Fri, 18 Oct 2013 10:35:56 +0200 blanchet make sure that registered code equations are actually equations
Tue, 01 Oct 2013 14:05:25 +0200 blanchet refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
Tue, 01 Oct 2013 14:05:25 +0200 blanchet renamed ML files
less more (0) tip