2014-09-04 hoelzl 2014-09-04 cleanup Wfrec; introduce dependent_wf/wellorder_choice
2014-09-04 blanchet 2014-09-04 tuned Nitpick and Refute examples, which are too slow on some testing machines
2014-09-04 blanchet 2014-09-04 tweaked setup for datatype realizer
2014-09-04 blanchet 2014-09-04 renamed internal constant
2014-09-04 blanchet 2014-09-04 moved code around
2014-09-04 blanchet 2014-09-04 tuned size function generation
2014-09-04 blanchet 2014-09-04 tuning
2014-09-03 blanchet 2014-09-03 introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
2014-09-03 blanchet 2014-09-03 tuned ctr_sugar database handling
2014-09-03 blanchet 2014-09-03 tuned BNF database handling
2014-09-03 blanchet 2014-09-03 intelligible errors instead of tactic failures
2014-09-03 blanchet 2014-09-03 reenabled yet another example
2014-09-03 blanchet 2014-09-03 made new tactic even more robust
2014-09-03 blanchet 2014-09-03 reenabled more examples
2014-09-03 blanchet 2014-09-03 fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)
2014-09-03 blanchet 2014-09-03 reintroduced more examples
2014-09-03 blanchet 2014-09-03 improved tactic further
2014-09-03 blanchet 2014-09-03 reenabled example
2014-09-03 blanchet 2014-09-03 improved new countability tactic
2014-09-03 blanchet 2014-09-03 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
2014-09-03 blanchet 2014-09-03 more robust exception handling
2014-09-03 blanchet 2014-09-03 added tests for new 'countable_datatype' proof method
2014-09-03 traytel 2014-09-03 lessen the burden on the caller: sort where necessary in n2m
2014-09-03 blanchet 2014-09-03 added compatibility function
2014-09-03 blanchet 2014-09-03 added countable tactic for new-style datatypes
2014-09-03 blanchet 2014-09-03 tuning
2014-09-03 blanchet 2014-09-03 registered 'typerep' as countable again
2014-09-03 blanchet 2014-09-03 moved old datatype material around
2014-09-03 blanchet 2014-09-03 removed vacuous theorem references
2014-09-03 blanchet 2014-09-03 commented out failing tactic (now that 'typerep' is defined using the new package
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