Sat, 06 Sep 2014 20:12:34 +0200 haftmann theory about lexicographic ordering on functions
Sat, 06 Sep 2014 20:12:32 +0200 haftmann added various facts
Fri, 05 Sep 2014 16:09:03 +0100 paulson Generalised card_length_listsum to all m
Fri, 05 Sep 2014 14:58:13 +0200 nipkow added lemma
Fri, 05 Sep 2014 00:41:01 +0200 blanchet updated docs
Fri, 05 Sep 2014 00:41:01 +0200 blanchet pretend code generation is a ctr_sugar plugin
Fri, 05 Sep 2014 00:41:01 +0200 blanchet updated docs
Fri, 05 Sep 2014 00:41:01 +0200 blanchet added 'plugins' option to control which hooks are enabled
Fri, 05 Sep 2014 00:41:01 +0200 blanchet introduced mechanism to filter interpretations
Fri, 05 Sep 2014 00:41:01 +0200 blanchet fixed infinite loops in 'register' functions + more uniform API
Fri, 05 Sep 2014 00:41:01 +0200 blanchet named interpretations
Fri, 05 Sep 2014 00:41:00 +0200 blanchet centralized and cleaned up naming handling
Thu, 04 Sep 2014 14:02:37 +0200 hoelzl cleanup Wfrec; introduce dependent_wf/wellorder_choice
Thu, 04 Sep 2014 11:53:39 +0200 blanchet tuned Nitpick and Refute examples, which are too slow on some testing machines
Thu, 04 Sep 2014 11:20:59 +0200 blanchet tweaked setup for datatype realizer
Thu, 04 Sep 2014 09:02:43 +0200 blanchet renamed internal constant
Thu, 04 Sep 2014 09:02:43 +0200 blanchet moved code around
Thu, 04 Sep 2014 09:02:43 +0200 blanchet tuned size function generation
Thu, 04 Sep 2014 09:02:36 +0200 blanchet tuning
Wed, 03 Sep 2014 22:49:05 +0200 blanchet introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
Wed, 03 Sep 2014 22:47:48 +0200 blanchet tuned ctr_sugar database handling
Wed, 03 Sep 2014 22:47:35 +0200 blanchet tuned BNF database handling
Wed, 03 Sep 2014 22:47:09 +0200 blanchet intelligible errors instead of tactic failures
Wed, 03 Sep 2014 22:47:05 +0200 blanchet reenabled yet another example
Wed, 03 Sep 2014 22:47:05 +0200 blanchet made new tactic even more robust
Wed, 03 Sep 2014 22:47:05 +0200 blanchet reenabled more examples
Wed, 03 Sep 2014 22:47:05 +0200 blanchet fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)
Wed, 03 Sep 2014 22:47:05 +0200 blanchet reintroduced more examples
Wed, 03 Sep 2014 22:47:05 +0200 blanchet improved tactic further
Wed, 03 Sep 2014 22:47:05 +0200 blanchet reenabled example
Wed, 03 Sep 2014 22:47:05 +0200 blanchet improved new countability tactic
Wed, 03 Sep 2014 22:47:05 +0200 blanchet 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
Wed, 03 Sep 2014 22:47:05 +0200 blanchet more robust exception handling
Wed, 03 Sep 2014 22:46:54 +0200 blanchet added tests for new 'countable_datatype' proof method
Wed, 03 Sep 2014 12:30:25 +0200 traytel lessen the burden on the caller: sort where necessary in n2m
Wed, 03 Sep 2014 09:43:00 +0200 blanchet added compatibility function
Wed, 03 Sep 2014 00:31:38 +0200 blanchet added countable tactic for new-style datatypes
Wed, 03 Sep 2014 00:31:37 +0200 blanchet tuning
Wed, 03 Sep 2014 00:06:32 +0200 blanchet registered 'typerep' as countable again
Wed, 03 Sep 2014 00:06:30 +0200 blanchet moved old datatype material around
Wed, 03 Sep 2014 00:06:28 +0200 blanchet removed vacuous theorem references
Wed, 03 Sep 2014 00:06:27 +0200 blanchet commented out failing tactic (now that 'typerep' is defined using the new package
Wed, 03 Sep 2014 00:06:26 +0200 blanchet tuned imports
Wed, 03 Sep 2014 00:06:25 +0200 blanchet use 'datatype_new'
Wed, 03 Sep 2014 00:06:24 +0200 blanchet use 'datatype_new' in 'Main'
Wed, 03 Sep 2014 00:06:23 +0200 blanchet take out 'x = C' of the simplifier for unit types
Wed, 03 Sep 2014 00:06:22 +0200 blanchet giving up calling 'datatype_compat' in a locale -- causes trouble with extensions
Wed, 03 Sep 2014 00:06:22 +0200 blanchet ported 'Statespace' to support new datatypes as well
Wed, 03 Sep 2014 00:06:21 +0200 blanchet use 'datatype_new' in Quickcheck examples
Wed, 03 Sep 2014 00:06:19 +0200 blanchet more compatibility functions
Wed, 03 Sep 2014 00:06:18 +0200 blanchet codatatypes are not datatypes
Wed, 03 Sep 2014 00:06:17 +0200 blanchet ported Quickcheck to support new datatypes better
Tue, 02 Sep 2014 23:59:49 +0200 blanchet removed more slow Refute tests
Tue, 02 Sep 2014 23:59:46 +0200 blanchet tuned Refute example
Tue, 02 Sep 2014 16:38:26 +0200 steckerm Some work on the new waldmeister integration
Tue, 02 Sep 2014 14:40:32 +0200 boehmes merged
Tue, 02 Sep 2014 14:40:14 +0200 boehmes replay Z3 rewrite steps that lift if-then-else expressions
Tue, 02 Sep 2014 13:40:03 +0200 traytel test discriminators/selectors in BNF regression suite
Tue, 02 Sep 2014 12:13:32 +0200 blanchet merge
Tue, 02 Sep 2014 12:11:04 +0200 blanchet made SML/NJ happier
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip