Thu, 25 Sep 2014 18:47:32 +0200 haftmann more correct precedence of do-notation
Thu, 25 Sep 2014 17:07:44 +0200 wenzelm merged
Thu, 25 Sep 2014 15:01:42 +0200 wenzelm save image as PNG or PDF;
Thu, 25 Sep 2014 12:22:12 +0200 wenzelm support for PNG output;
Thu, 25 Sep 2014 10:36:39 +0200 wenzelm more isatests (on lxbroy4);
Thu, 25 Sep 2014 16:35:56 +0200 desharna document 'corec_transfer'
Thu, 25 Sep 2014 16:35:56 +0200 desharna generate 'corec_transfer' for codatatypes
Thu, 25 Sep 2014 16:35:54 +0200 desharna document 'rec_transfer'
Thu, 25 Sep 2014 16:35:53 +0200 desharna generate 'rec_transfer' for datatypes
Thu, 25 Sep 2014 16:35:51 +0200 desharna generate 'dtor_corec_transfer' for codatatypes
Thu, 25 Sep 2014 16:35:50 +0200 desharna generate 'ctor_rec_transfer' for datatypes
Mon, 01 Sep 2014 14:14:47 +0200 traytel goal generation for xtor_co_rec_transfer
Thu, 25 Sep 2014 13:30:57 +0200 blanchet commented out some tests that require external tools (e.g. ghc)
Thu, 25 Sep 2014 13:30:57 +0200 blanchet added useful options to CVC4
Thu, 25 Sep 2014 12:27:34 +0200 traytel subscribe for isatest
Thu, 25 Sep 2014 09:01:14 +0200 traytel even more deads go to the end (continuation of e3a01b73579f)
Thu, 25 Sep 2014 11:38:56 +0200 nipkow added function size1
Wed, 24 Sep 2014 19:11:21 +0200 haftmann added lemmas
Wed, 24 Sep 2014 19:10:30 +0200 haftmann tuned
Wed, 24 Sep 2014 21:00:07 +0200 blanchet avoid type variable name clash
Wed, 24 Sep 2014 21:00:07 +0200 blanchet tuning
Wed, 24 Sep 2014 17:33:53 +0200 blanchet made N2M tests conditional, since they appear to cause Isatest timeouts and are kind of slow
Wed, 24 Sep 2014 16:35:42 +0200 blanchet improved 'bnf' parser
Wed, 24 Sep 2014 15:46:41 +0200 blanchet updated SMT certificates
Wed, 24 Sep 2014 15:46:40 +0200 blanchet allow homogeneous nesting for SMT (co)datatypes
Wed, 24 Sep 2014 15:46:25 +0200 blanchet interleave (co)datatypes in the right order w.r.t. dependencies
Wed, 24 Sep 2014 15:46:24 +0200 blanchet rule out nested (co)recursion for SMT (co)datatypes
Wed, 24 Sep 2014 15:46:23 +0200 blanchet gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
Wed, 24 Sep 2014 15:46:11 +0200 blanchet tuning
Wed, 24 Sep 2014 15:45:55 +0200 blanchet simpler proof
Wed, 24 Sep 2014 11:09:05 +0200 nipkow added nice standard syntax
Mon, 22 Sep 2014 21:45:59 +0200 wenzelm clarified timeout for isatest;
Mon, 22 Sep 2014 21:31:45 +0200 wenzelm merged
Mon, 22 Sep 2014 21:28:57 +0200 wenzelm discontinued old "xnum" token category;
Mon, 22 Sep 2014 17:07:18 +0200 wenzelm added csdp-6.x for proof method (sos csdp);
Mon, 22 Sep 2014 16:28:24 +0200 wenzelm examples for local CSDP executable;
Mon, 22 Sep 2014 16:15:29 +0200 wenzelm clarified SOS tool setup vs. examples;
Mon, 22 Sep 2014 15:01:27 +0200 desharna make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
Mon, 22 Sep 2014 10:55:51 +0200 wenzelm merged
Mon, 22 Sep 2014 10:18:41 +0200 wenzelm clarified ISABELLE_POLYML;
Mon, 22 Sep 2014 10:53:54 +0200 Andreas Lochbihler drop workaround addressed by d0d3c30806b4
Sun, 21 Sep 2014 20:22:12 +0200 wenzelm renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
Sun, 21 Sep 2014 20:14:04 +0200 wenzelm more standard Isabelle/ML operations;
Sun, 21 Sep 2014 19:53:50 +0200 wenzelm tuned;
Sun, 21 Sep 2014 16:56:11 +0200 haftmann explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
Sun, 21 Sep 2014 16:56:06 +0200 haftmann corrected slip in documentation
Sat, 20 Sep 2014 10:44:24 +0200 steckerm Removed double space
Sat, 20 Sep 2014 10:44:24 +0200 steckerm Changed proof method to auto for custom Waldmeister lemma
Sat, 20 Sep 2014 10:44:24 +0200 steckerm Minor fixes in ATP_Waldmeister
Sat, 20 Sep 2014 10:44:23 +0200 steckerm Made encoded type for apply less restrictive
Sat, 20 Sep 2014 10:44:23 +0200 steckerm Updated fix_name function
Sat, 20 Sep 2014 10:42:08 +0200 steckerm Added support for partial function application
Sat, 20 Sep 2014 10:42:08 +0200 steckerm Improved equality handling in skolemization
Sat, 20 Sep 2014 10:42:08 +0200 steckerm Re-added hypothesis argument to problem generation
Thu, 18 Sep 2014 18:48:54 +0200 haftmann always annotate potentially polymorphic Haskell numerals
Thu, 18 Sep 2014 18:48:04 +0200 haftmann tuned
Thu, 18 Sep 2014 18:48:04 +0200 haftmann simplified and tuned using signed_string_of_int
Thu, 18 Sep 2014 18:48:04 +0200 haftmann tuned data structure
Fri, 19 Sep 2014 14:24:03 +0200 blanchet tuning
Fri, 19 Sep 2014 14:08:21 +0200 blanchet documented limitations
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip