src/HOL/Tools/ctr_sugar.ML
Tue, 12 Nov 2013 13:47:24 +0100 blanchet export useful ML function
Tue, 12 Nov 2013 13:47:24 +0100 blanchet tuned headers
Tue, 12 Nov 2013 13:47:24 +0100 blanchet moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction
less more (0) tip