src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
2012-09-08 blanchet 2012-09-08 some work on coiter tactic
2012-09-08 blanchet 2012-09-08 more sugar on codatatypes
2012-09-05 blanchet 2012-09-05 by default, only generate one discriminator for a two-value datatype
2012-09-05 blanchet 2012-09-05 code indentation
2012-09-05 blanchet 2012-09-05 ported "Misc_Data" to new syntax
2012-09-05 blanchet 2012-09-05 made "mk_case_eq_tac" work in the case where the first constructor is an "alternate" constructor (in which case its discriminator paradoxically starts with a negation)
2012-09-05 blanchet 2012-09-05 reindented code
2012-09-05 blanchet 2012-09-05 fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case
2012-09-05 blanchet 2012-09-05 fixed bugs in one-constructor case
2012-09-04 blanchet 2012-09-04 renamed "disc_exclus" theorem to "disc_exclude"
2012-09-04 blanchet 2012-09-04 renamed theorem
2012-09-04 blanchet 2012-09-04 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
2012-09-03 blanchet 2012-09-03 rearrange dependencies
2012-09-03 blanchet 2012-09-03 renamed three BNF/(co)datatype-related commands