src/Doc/Datatypes/Datatypes.thy
2014-01-24 blanchet 2014-01-24 killed 'More_BNFs' by moving its various bits where they (now) belong
2014-01-22 wenzelm 2014-01-22 merged
2014-01-22 wenzelm 2014-01-22 prefer rail cartouche -- avoid back-slashed quotes; proper documentation of \<newline> syntax;
2014-01-20 blanchet 2014-01-20 dissolved BNF session
2014-01-20 blanchet 2014-01-20 reduced dependencies + updated docs
2014-01-17 wenzelm 2014-01-17 clarified @{rail} syntax: prefer explicit \<newline> symbol;
2014-01-09 panny 2014-01-09 do not use wrong constructor in auto-generated proof goal
2014-01-09 blanchet 2014-01-09 reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
2013-12-19 blanchet 2013-12-19 implemented 'exhaustive' option in tactic
2013-12-02 blanchet 2013-12-02 added 'no_code' option
2013-12-02 blanchet 2013-12-02 revert making 'map_cong' a 'cong' -- it breaks too many proofs in the AFP
2013-12-02 blanchet 2013-12-02 docs for forgotten BNF theorems
2013-12-02 blanchet 2013-12-02 minor doc update
2013-11-27 traytel 2013-11-27 some documentation
2013-11-20 blanchet 2013-11-20 fixed LaTeX missing }
2013-11-19 blanchet 2013-11-19 updated docs
2013-11-19 blanchet 2013-11-19 case_if -> case_eq_if + docs
2013-11-13 blanchet 2013-11-13 shortened generated property name
2013-11-13 traytel 2013-11-13 more explicit syntax for defining a bnf
2013-11-12 blanchet 2013-11-12 document idiomatic use of 'simps_of_case'
2013-11-11 blanchet 2013-11-11 minor doc fix
2013-11-07 blanchet 2013-11-07 more docs
2013-11-06 blanchet 2013-11-06 update docs
2013-10-27 blanchet 2013-10-27 commented out vaporware
2013-10-22 traytel 2013-10-22 update doc according to c0186a0d8cb3
2013-10-21 blanchet 2013-10-21 more doc -- feedback from Andrei P.
2013-10-21 blanchet 2013-10-21 more docs
2013-10-21 blanchet 2013-10-21 more docs
2013-10-21 blanchet 2013-10-21 more docs
2013-10-21 blanchet 2013-10-21 expand doc a bit
2013-10-21 blanchet 2013-10-21 updated doc
2013-10-18 blanchet 2013-10-18 updated docs
2013-10-18 blanchet 2013-10-18 doc fixes suggested by Andreas L.
2013-10-07 blanchet 2013-10-07 more primcorec docs
2013-10-07 blanchet 2013-10-07 minor doc fix
2013-10-02 blanchet 2013-10-02 more (co)data docs
2013-10-02 blanchet 2013-10-02 minor doc fix (there is no guarantee that the equations for a given f_i are contiguous in the collection)
2013-10-01 traytel 2013-10-01 base the fset bnf on the new FSet theory
2013-09-30 blanchet 2013-09-30 more "primrec_new" documentation
2013-09-26 blanchet 2013-09-26 generate "sel_splits(_asm)" theorems
2013-09-26 blanchet 2013-09-26 generate "sel_exhaust" theorem
2013-09-25 blanchet 2013-09-25 textual improvements following Christian Sternagel's feedback
2013-09-24 blanchet 2013-09-24 renamed generated property
2013-09-24 blanchet 2013-09-24 updated docs
2013-09-24 panny 2013-09-24 support "of" syntax to disambiguate selector equations
2013-09-24 blanchet 2013-09-24 more (co)data docs
2013-09-24 blanchet 2013-09-24 improved rail diagram
2013-09-24 blanchet 2013-09-24 use "primcorec" in doc
2013-09-24 panny 2013-09-24 add "primcorec" command (cf. ae7f50e70c09)
2013-09-23 blanchet 2013-09-23 added [code] to selectors
2013-09-23 blanchet 2013-09-23 set [code] on case equations
2013-09-20 blanchet 2013-09-20 renamed "primcorec" to "primcorecursive", to open the door to a 'theory -> theory' command called "primcorec" (cf. "fun" vs. "function")
2013-09-20 blanchet 2013-09-20 more primcorec docs
2013-09-20 blanchet 2013-09-20 added primcorec examples with lambdas
2013-09-20 blanchet 2013-09-20 more primcorec docs
2013-09-20 blanchet 2013-09-20 adapted primcorec documentation to reflect the three views
2013-09-20 blanchet 2013-09-20 updated docs
2013-09-19 panny 2013-09-19 generate more theorems (e.g. for types with only one constructor)
2013-09-18 blanchet 2013-09-18 updated docs
2013-09-18 blanchet 2013-09-18 use singular to avoid confusion