src/Doc/Datatypes/Datatypes.thy
2014-08-18 blanchet 2014-08-18 added collection theorem for consistency and convenience
2014-08-18 blanchet 2014-08-18 reordered some (co)datatype property names for more consistency
2014-08-18 desharna 2014-08-18 document 'map_cong_simp'
2014-08-18 desharna 2014-08-18 document 'inj_map_strong'
2014-08-18 desharna 2014-08-18 note 'inj_map' more often
2014-08-14 desharna 2014-08-14 document property 'rel_map'
2014-08-12 desharna 2014-08-12 document property 'set_cases'
2014-08-12 desharna 2014-08-12 document property 'set_intros'
2014-07-30 desharna 2014-07-30 document property 'set_induct'
2014-07-19 blanchet 2014-07-19 doc fixes (contributed by Christian Sternagel)
2014-07-16 desharna 2014-07-16 document property 'rel_sel'
2014-07-15 blanchet 2014-07-15 took out 'rel_cases' for now because of failing tactic
2014-07-11 blanchet 2014-07-11 more docs
2014-07-07 desharna 2014-07-07 document property 'rel_cases'
2014-07-03 desharna 2014-07-03 document property 'rel_intros'
2014-07-02 desharna 2014-07-02 document property 'corec_code'
2014-07-01 desharna 2014-07-01 document property 'rel_induct'
2014-06-27 blanchet 2014-06-27 merged two small theory files
2014-06-24 desharna 2014-06-24 document property 'rel_coinduct'
2014-06-10 blanchet 2014-06-10 changed syntax of map: and rel: arguments to BNF-based datatypes
2014-06-10 blanchet 2014-06-10 use 'where' clause for selector default value syntax
2014-06-02 desharna 2014-06-02 document property 'sel_set'
2014-05-27 blanchet 2014-05-27 don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
2014-05-26 blanchet 2014-05-26 changed '-:' to 'dead' in BNF
2014-05-26 blanchet 2014-05-26 got rid of '=:' squiggly
2014-05-26 blanchet 2014-05-26 document '=:' syntax better
2014-05-23 blanchet 2014-05-23 added fifth member to BNF team
2014-05-21 desharna 2014-05-21 document property 'sel_map'
2014-05-19 blanchet 2014-05-19 hide more consts to beautify documentation
2014-05-19 desharna 2014-05-19 document property 'disc_map_iff'
2014-05-14 desharna 2014-05-14 document 'set_empty'
2014-05-08 desharna 2014-05-08 document 'map_id0'
2014-05-13 blanchet 2014-05-13 more bnf_decl -> bnf_axiomatization
2014-05-13 blanchet 2014-05-13 tuned docs
2014-05-13 traytel 2014-05-13 bnf_decl -> bnf_axiomatization
2014-05-08 desharna 2014-05-08 Documented new property
2014-04-23 blanchet 2014-04-23 updated BNF docs
2014-04-23 blanchet 2014-04-23 tuned doc comment
2014-04-23 blanchet 2014-04-23 updated docs
2014-03-14 blanchet 2014-03-14 tuned wording (pun)
2014-03-14 blanchet 2014-03-14 document the new 'nonexhaustive' option (cf. 52e8f110fec3)
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-04 blanchet 2014-03-04 minor doc fix
2014-03-03 blanchet 2014-03-03 removed (co)iterators from documentation
2014-02-23 blanchet 2014-02-23 updated docs
2014-02-21 blanchet 2014-02-21 renamed 'recs' and 'cases' theorems 'rec' and 'case' in old datatype package, for consistency with new package
2014-02-17 blanchet 2014-02-17 renamed 'datatype_new_compat' to 'datatype_compat'
2014-02-17 blanchet 2014-02-17 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
2014-02-14 blanchet 2014-02-14 more (co)datatype docs
2014-02-14 blanchet 2014-02-14 updated docs to reflect the new 'free_constructors' syntax
2014-02-14 blanchet 2014-02-14 renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
2014-02-13 blanchet 2014-02-13 added a bit of documentation for the different commands
2014-02-13 blanchet 2014-02-13 cleaner, complete proof in documentation, contributed by Dmitriy T.
2014-02-12 blanchet 2014-02-12 killed 'rep_compat' option
2014-02-12 blanchet 2014-02-12 updated docs
2014-02-07 blanchet 2014-02-07 more docs
2014-02-07 blanchet 2014-02-07 more docs
2014-02-07 blanchet 2014-02-07 docs
2014-02-06 blanchet 2014-02-06 docs
2014-02-06 blanchet 2014-02-06 docs about registering a BNF