2014-09-17 blanchet 2014-09-17 added interface for CVC4 extensions
2014-09-17 blanchet 2014-09-17 avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')
2014-09-17 blanchet 2014-09-17 tweaked compatibility layer
2014-09-17 blanchet 2014-09-17 avoid clash with Quickcheck's generated 'random_xxx' function
2014-09-17 blanchet 2014-09-17 added missing 'restore' in 'transfer' plugin
2014-09-17 blanchet 2014-09-17 syntactic check to determine when to prove 'nested_size_o_map'
2014-09-17 blanchet 2014-09-17 support (finite values of) codatatypes in Quickcheck
2014-09-16 blanchet 2014-09-16 tuned fact visibility
2014-09-16 blanchet 2014-09-16 register 'prod' and 'sum' as datatypes, to allow N2M through them
2014-09-16 blanchet 2014-09-16 took out 'old_datatype' examples -- those just cause timeouts in Isatests
2014-09-16 blanchet 2014-09-16 added 'extraction' plugins -- this might help 'HOL-Proofs'
2014-09-16 nipkow 2014-09-16 added lemma
2014-09-16 Andreas Lochbihler 2014-09-16 add target language evaluators for the value command; drop obsolete command eval_term
2014-09-15 blanchet 2014-09-15 tuning
2014-09-15 blanchet 2014-09-15 refactoring
2014-09-15 blanchet 2014-09-15 tuning
2014-09-15 blanchet 2014-09-15 set 'mono' attribute on 'rel_mono'
2014-09-15 blanchet 2014-09-15 'code' is needed for extraction datatype
2014-09-15 blanchet 2014-09-15 tuning
2014-09-15 blanchet 2014-09-15 removed accidental '@{print}'
2014-09-15 blanchet 2014-09-15 tuning
2014-09-15 blanchet 2014-09-15 more hints on how to port 'size'
2014-09-15 blanchet 2014-09-15 tuned definition of 'size' function to get nicer properties
2014-09-15 blanchet 2014-09-15 tuning
2014-09-15 blanchet 2014-09-15 document size difference
2014-09-15 blanchet 2014-09-15 generate 'code' attribute only if 'code' plugin is enabled
2014-09-14 blanchet 2014-09-14 disable datatype 'plugins' for internal types
2014-09-13 blanchet 2014-09-13 ported Imperative HOL to new datatypes
2014-09-13 blanchet 2014-09-13 imported patch phantoms
2014-09-12 blanchet 2014-09-12 enabled 'Sudoku' only with 'ISABELLE_FULL_TEST' -- Sudoku is fast enough on modern hardware (within seconds on my MacBook), but it seems to fail on older test machines
2014-09-12 blanchet 2014-09-12 new datatype is too slow on the huge datatypes (at least the mutual ones) -- use 'old_datatype' instead
2014-09-12 blanchet 2014-09-12 run larger nominal examples only 'ISABELLE_FULL_TEST'
2014-09-12 desharna 2014-09-12 refactor repeated terms in a single variable
2014-09-12 desharna 2014-09-12 make 'ctr_transfer' tactic more robust
2014-09-12 desharna 2014-09-12 make 'rel_sel' and 'map_sel' tactics more robust
2014-09-12 fleury 2014-09-12 Changing the way the dependencies are managed.
2014-09-12 fleury 2014-09-12 correction in the thf0 parser ("(=)" found in a Satallax proof).
2014-09-12 blanchet 2014-09-12 merge
2014-09-12 blanchet 2014-09-12 fixed spellings
2014-09-12 haftmann 2014-09-12 NEWS
2014-09-11 haftmann 2014-09-11 abstract product over monoid for lists
2014-09-11 haftmann 2014-09-11 use proto_base_sort uniformly
2014-09-11 blanchet 2014-09-11 fixed some spelling mistakes
2014-09-11 blanchet 2014-09-11 tuned comment
2014-09-11 blanchet 2014-09-11 more porting to new datatypes
2014-09-11 blanchet 2014-09-11 tuning terminology
2014-09-11 blanchet 2014-09-11 compile
2014-09-11 blanchet 2014-09-11 renamed example theory for consistency
2014-09-11 blanchet 2014-09-11 updated ROOT
2014-09-11 blanchet 2014-09-11 tuned documentation
2014-09-11 blanchet 2014-09-11 updated news
2014-09-11 blanchet 2014-09-11 renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
2014-09-11 blanchet 2014-09-11 move datatype benchmarks
2014-09-11 blanchet 2014-09-11 use new datatypes for benchmarks
2014-09-11 blanchet 2014-09-11 renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
2014-09-11 blanchet 2014-09-11 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
2014-09-11 blanchet 2014-09-11 tuning
2014-09-11 blanchet 2014-09-11 fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
2014-09-11 blanchet 2014-09-11 tuning
2014-09-11 blanchet 2014-09-11 fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'