src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
Tue, 04 Sep 2012 13:06:41 +0200 more work on sugar + simplify Trueprop + eq idiom everywhere