2014-09-03 blanchet 2014-09-03 tuned imports
2014-09-03 blanchet 2014-09-03 use 'datatype_new'
2014-09-03 blanchet 2014-09-03 use 'datatype_new' in 'Main'
2014-09-03 blanchet 2014-09-03 take out 'x = C' of the simplifier for unit types
2014-09-03 blanchet 2014-09-03 giving up calling 'datatype_compat' in a locale -- causes trouble with extensions
2014-09-03 blanchet 2014-09-03 ported 'Statespace' to support new datatypes as well
2014-09-03 blanchet 2014-09-03 use 'datatype_new' in Quickcheck examples
2014-09-03 blanchet 2014-09-03 more compatibility functions
2014-09-03 blanchet 2014-09-03 codatatypes are not datatypes
2014-09-03 blanchet 2014-09-03 ported Quickcheck to support new datatypes better
2014-09-02 blanchet 2014-09-02 removed more slow Refute tests
2014-09-02 blanchet 2014-09-02 tuned Refute example
2014-09-02 steckerm 2014-09-02 Some work on the new waldmeister integration
2014-09-02 boehmes 2014-09-02 merged
2014-09-02 boehmes 2014-09-02 replay Z3 rewrite steps that lift if-then-else expressions
2014-09-02 traytel 2014-09-02 test discriminators/selectors in BNF regression suite
2014-09-02 blanchet 2014-09-02 merge
2014-09-02 blanchet 2014-09-02 made SML/NJ happier
2014-09-02 blanchet 2014-09-02 tuning
2014-09-02 traytel 2014-09-02 silenced nonexhaustive primrec warnings
2014-09-02 haftmann 2014-09-02 more convenient printing of real numbers after evaluation
2014-09-01 blanchet 2014-09-01 avoid more 'bad background theory' issues
2014-09-01 blanchet 2014-09-01 ported TFL to mixture of old and new datatypes
2014-09-01 blanchet 2014-09-01 drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
2014-09-01 blanchet 2014-09-01 ported to use new-style datatypes * * * compile
2014-09-01 blanchet 2014-09-01 ported Refute to use new datatypes when possible
2014-09-01 blanchet 2014-09-01 renamed BNF theories
2014-09-01 blanchet 2014-09-01 renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
2014-09-01 blanchet 2014-09-01 added primrec compatibility function
2014-09-01 blanchet 2014-09-01 more work on compatibility interfaces
2014-09-01 blanchet 2014-09-01 added compatibility examples/tests
2014-09-01 blanchet 2014-09-01 implemented compatibility definition of datatype
2014-09-01 blanchet 2014-09-01 implemented compatibility interpretation
2014-09-01 blanchet 2014-09-01 compile
2014-09-01 blanchet 2014-09-01 compile
2014-09-01 blanchet 2014-09-01 tuning
2014-09-01 blanchet 2014-09-01 compile
2014-09-01 blanchet 2014-09-01 more compatibility between old- and new-style datatypes
2014-09-01 blanchet 2014-09-01 added theory-based getters for convenience
2014-09-01 blanchet 2014-09-01 made transfer functions slightly more general
2014-09-01 blanchet 2014-09-01 tuned signatures
2014-09-01 blanchet 2014-09-01 tuning
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-09-01 blanchet 2014-09-01 tuned structure inclusion
2014-09-01 blanchet 2014-09-01 took out legacy material from 'HOL/Library/Library.thy'
2014-09-01 blanchet 2014-09-01 removed commented out parts
2014-09-01 blanchet 2014-09-01 tuned whitespace
2014-09-01 desharna 2014-09-01 document 'set_transfer'
2014-09-01 desharna 2014-09-01 generate 'set_transfer' for BNFs
2014-09-01 desharna 2014-09-01 document 'rel_transfer'
2014-09-01 desharna 2014-09-01 generate 'rel_transfer' for BNFs
2014-09-01 desharna 2014-09-01 document 'map_transfer'
2014-09-01 desharna 2014-09-01 note 'map_transfer' more often
2014-08-31 haftmann 2014-08-31 separated listsum material
2014-08-31 haftmann 2014-08-31 restored generic value slot, retaining default behaviour and separate approximate command
2014-08-31 haftmann 2014-08-31 convenient printing of (- 1 :: integer) after code evaluation
2014-08-30 haftmann 2014-08-30 inlined unused definition
2014-08-29 hoelzl 2014-08-29 add simp rules for divisions of numerals in floor and ceiling.
2014-08-29 desharna 2014-08-29 document 'disc_transfer'
2014-08-29 desharna 2014-08-29 generate 'disc_transfer' for (co)datatypes