2012-08-30 blanchet [Thu, 30 Aug 2012 14:27:26 +0200] rev 49029
generate "disc_exhaust" property
src/HOL/Codatatype/Tools/bnf_gfp.ML src/HOL/Codatatype/Tools/bnf_lfp.ML src/HOL/Codatatype/Tools/bnf_sugar.ML src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML

2012-08-30 blanchet [Thu, 30 Aug 2012 13:42:05 +0200] rev 49028
generate "disc_distinct" theorems
src/HOL/Codatatype/Tools/bnf_sugar.ML src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML

2012-08-30 blanchet [Thu, 30 Aug 2012 11:31:47 +0200] rev 49027
added discriminator theorems
src/HOL/Codatatype/Tools/bnf_sugar.ML

2012-08-30 blanchet [Thu, 30 Aug 2012 11:31:20 +0200] rev 49026
adjust example
src/HOL/Nitpick_Examples/minipick.ML

2012-08-30 blanchet [Thu, 30 Aug 2012 09:48:27 +0200] rev 49025
more work on sugar
src/HOL/Codatatype/Tools/bnf_sugar.ML

2012-08-30 blanchet [Thu, 30 Aug 2012 09:47:46 +0200] rev 49024
updated Java-related error message
src/HOL/Tools/Nitpick/kodkod.ML src/HOL/Tools/Nitpick/nitpick.ML

2012-08-30 blanchet [Thu, 30 Aug 2012 09:47:46 +0200] rev 49023
changed order of arguments to "bnf_sugar"
src/HOL/Codatatype/Tools/bnf_sugar.ML

2012-08-30 blanchet [Thu, 30 Aug 2012 09:47:46 +0200] rev 49022
define selectors and discriminators
src/HOL/Codatatype/Tools/bnf_sugar.ML src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML

2012-08-30 blanchet [Thu, 30 Aug 2012 09:47:46 +0200] rev 49021
tuning
src/HOL/Codatatype/Tools/bnf_def.ML

2012-08-30 blanchet [Thu, 30 Aug 2012 09:47:46 +0200] rev 49020
more work on BNF sugar -- up to derivation of nchotomy
etc/isar-keywords.el src/HOL/Codatatype/Codatatype.thy src/HOL/Codatatype/Tools/bnf_fp_util.ML src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML src/HOL/Codatatype/Tools/bnf_gfp_util.ML src/HOL/Codatatype/Tools/bnf_sugar.ML src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML src/HOL/Tools/Datatype/rep_datatype.ML