2014-08-25 Andreas Lochbihler 2014-08-25 add testing framework for generated code
2014-08-25 Andreas Lochbihler 2014-08-25 correct code equation for term_of on integer
2014-08-25 Andreas Lochbihler 2014-08-25 merged
2014-08-22 Andreas Lochbihler 2014-08-22 add code equation for term_of on integer
2014-08-22 blanchet 2014-08-22 added lemmas contributed by Rene Thiemann
2014-08-22 wenzelm 2014-08-22 attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";
2014-08-22 wenzelm 2014-08-22 tuned whitespace;
2014-08-22 wenzelm 2014-08-22 clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;
2014-08-22 wenzelm 2014-08-22 merged
2014-08-22 wenzelm 2014-08-22 made SML/NJ happy;
2014-08-21 wenzelm 2014-08-21 clarified Method.section: explicit declaration with static closure;
2014-08-21 wenzelm 2014-08-21 tuned signature -- define some elementary operations earlier;
2014-08-21 wenzelm 2014-08-21 discontinued odd "temporary" workaround from 2006 (6ac7a4fc32a0), which has no measurable relevance;
2014-08-21 wenzelm 2014-08-21 tuned;
2014-08-21 wenzelm 2014-08-21 tuned;
2014-08-21 wenzelm 2014-08-21 tuned;
2014-08-22 haftmann 2014-08-22 generic euclidean algorithm (due to Manuel Eberl)
2014-08-21 haftmann 2014-08-21 integrated appendix theory into main theory; tuned ML
2014-08-21 haftmann 2014-08-21 dropped dead file
2014-08-21 desharna 2014-08-21 fix tactic failure with rel_induct0 minimal example: datatype_new 'a A1 = A1 nat and 'a A2 = A2 'a
2014-08-20 wenzelm 2014-08-20 added jdk-8u20 (inactive);
2014-08-20 wenzelm 2014-08-20 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
2014-08-20 wenzelm 2014-08-20 support for declaration within token source;
2014-08-20 wenzelm 2014-08-20 more uniform data slot;
2014-08-20 wenzelm 2014-08-20 default command position is only valid for default text chunk (amending dcb758188aa6);
2014-08-20 wenzelm 2014-08-20 tuned -- more total;
2014-08-20 wenzelm 2014-08-20 tuned;
2014-08-20 wenzelm 2014-08-20 support for nested Token.src within Token.T; tuned signature;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-08-19 wenzelm 2014-08-19 merged
2014-08-19 wenzelm 2014-08-19 clarified modules;
2014-08-19 wenzelm 2014-08-19 added PARALLEL_ALLGOALS convenience;
2014-08-19 wenzelm 2014-08-19 just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
2014-08-19 wenzelm 2014-08-19 tuned signature;
2014-08-19 wenzelm 2014-08-19 more compact datatypes;
2014-08-19 wenzelm 2014-08-19 tuned;
2014-08-19 wenzelm 2014-08-19 clarifed Method.evaluate: turn text into semantic method (like Basic);
2014-08-19 wenzelm 2014-08-19 simplified type Proof.method;
2014-08-18 wenzelm 2014-08-18 more general dummy: may contain "parked arguments", for example;
2014-08-19 desharna 2014-08-19 document 'ctr_transfer'
2014-08-19 desharna 2014-08-19 generate 'ctr_transfer' for (co)datatypes
2014-08-19 Andreas Lochbihler 2014-08-19 rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
2014-08-19 Andreas Lochbihler 2014-08-19 Enum.finite_5 already provides a non-distributive lattice (see 51aa30c9ee4e)
2014-08-19 blanchet 2014-08-19 reduced dependency on 'Datatype' theory and ML module
2014-08-19 blanchet 2014-08-19 removed Z3 3.2, now superseded by Z3 4.3
2014-08-19 blanchet 2014-08-19 avoid old 'smt' method in examples
2014-08-19 blanchet 2014-08-19 robustified tactics
2014-08-19 blanchet 2014-08-19 tuning
2014-08-19 blanchet 2014-08-19 don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
2014-08-19 blanchet 2014-08-19 documented slight incompatibility in NEWS
2014-08-18 blanchet 2014-08-18 removed junk
2014-08-18 blanchet 2014-08-18 updated docs
2014-08-18 blanchet 2014-08-18 set attributes on 'set_cases' theorem
2014-08-18 blanchet 2014-08-18 cleaned up derivation of 'sset_induct'
2014-08-18 blanchet 2014-08-18 tuning
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 generate 'map_cong_simp' for BNFs
2014-08-18 wenzelm 2014-08-18 merged