Wed, 30 Jul 2014 16:44:54 +0200 kuncar update documentation for Lifting/Transfer
Wed, 30 Jul 2014 16:44:54 +0200 kuncar add Isabelle Datatype Manual to the bibliography
Wed, 30 Jul 2014 21:40:19 +0200 wenzelm CONTRIBUTORS;
Wed, 30 Jul 2014 16:44:54 +0200 kuncar NEWS
Tue, 29 Jul 2014 17:13:25 +0200 hoelzl better ordering of positive_integral renaming to nn_integral in NEWS
Mon, 28 Jul 2014 12:31:30 +0200 desharna made tactic more robust w.r.t. dead variables; tuned;
Sun, 27 Jul 2014 21:20:11 +0200 blanchet do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
Mon, 28 Jul 2014 11:03:28 +0200 wenzelm some actual workaround to remove document nodes;
Sun, 27 Jul 2014 15:40:19 +0200 wenzelm Added tag Isabelle2014-RC1 for changeset c0fd03d13d28
Sat, 09 Aug 2014 21:03:42 +0200 wenzelm tuned;
Sat, 09 Aug 2014 07:59:15 +0200 nipkow tuned
Fri, 08 Aug 2014 17:36:08 +0200 Andreas Lochbihler add complete_lattice instances for Enum.finite_* types such that quickcheck deals with lattice class operations
Fri, 08 Aug 2014 08:26:32 +0200 nipkow tuned
Thu, 07 Aug 2014 12:17:41 +0200 blanchet no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
Thu, 07 Aug 2014 12:17:41 +0200 blanchet generate nicer 'set' theorems for (co)datatypes
Thu, 07 Aug 2014 12:17:41 +0200 blanchet compile
Thu, 07 Aug 2014 12:17:41 +0200 blanchet took out test driver
Thu, 07 Aug 2014 12:17:41 +0200 blanchet make TPTP tools work on polymorphic (TFF1) problems as well
Thu, 07 Aug 2014 12:17:41 +0200 blanchet put comments between TPTP lines to comply with TPTP BNF
Thu, 07 Aug 2014 12:17:41 +0200 blanchet test driver
Thu, 07 Aug 2014 12:17:41 +0200 blanchet treat variables as frees in 'conjecture's
Thu, 07 Aug 2014 12:17:41 +0200 blanchet support TFF1 in TPTP parser/interpreter
Thu, 07 Aug 2014 12:17:41 +0200 blanchet tuning
Thu, 07 Aug 2014 09:35:31 +0200 traytel tuned
Thu, 07 Aug 2014 10:06:18 +0200 nipkow tuned
Thu, 07 Aug 2014 09:48:04 +0200 nipkow tuned
Wed, 06 Aug 2014 18:20:31 +0200 traytel merged
Wed, 06 Aug 2014 16:00:11 +0200 traytel handle deep nesting in N2M
Wed, 06 Aug 2014 10:20:50 +0200 traytel made tactic more robust
Wed, 06 Aug 2014 18:03:43 +0200 nipkow added lemma
Wed, 06 Aug 2014 08:18:35 +0200 nipkow replaced misleading - by _
Tue, 05 Aug 2014 20:25:12 +0200 blanchet more correct clique computation for N2M
Tue, 05 Aug 2014 15:55:39 +0200 blanchet regenerated ML-Lex/Yacc files
Tue, 05 Aug 2014 15:54:47 +0200 blanchet correctly interpret arithmetic types
Tue, 05 Aug 2014 14:02:47 +0200 blanchet added 'datatype_compat' tests
Tue, 05 Aug 2014 13:52:35 +0200 blanchet tuning whitespace
Tue, 05 Aug 2014 11:07:53 +0200 blanchet tuned skolemization
Tue, 05 Aug 2014 10:59:40 +0200 blanchet rationalize Skolem names
Tue, 05 Aug 2014 10:17:15 +0200 blanchet tuning
Tue, 05 Aug 2014 10:02:35 +0200 blanchet tuned code
Tue, 05 Aug 2014 09:58:23 +0200 blanchet don't rename variables which will be renamed later anyway
Tue, 05 Aug 2014 09:55:42 +0200 blanchet normalize skolem argument variable names so that they coincide when taking the conjunction
Tue, 05 Aug 2014 09:20:00 +0200 blanchet tuning
Mon, 04 Aug 2014 16:55:03 +0200 blanchet tuned comments
Mon, 04 Aug 2014 16:53:09 +0200 blanchet deal with E definitions
Mon, 04 Aug 2014 15:08:13 +0200 blanchet updated 'compress' docs
Mon, 04 Aug 2014 15:02:02 +0200 blanchet cleaner 'compress' option
Mon, 04 Aug 2014 14:19:43 +0200 blanchet renamed 'sh_minimize' to 'minimize'; compile;
Mon, 04 Aug 2014 13:48:05 +0200 blanchet restored more sorting
Mon, 04 Aug 2014 13:16:18 +0200 blanchet tuned terminology (cf. 'isar_proofs' option)
Mon, 04 Aug 2014 13:13:10 +0200 blanchet sort facts in minimizer as well
Mon, 04 Aug 2014 13:06:24 +0200 blanchet default on 'metis' for ATPs if preplaying is disabled
Mon, 04 Aug 2014 12:52:48 +0200 blanchet more informative preplay failures
Mon, 04 Aug 2014 12:28:42 +0200 blanchet rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
Mon, 04 Aug 2014 11:54:23 +0200 blanchet slightly earlier exit from preplaying
Mon, 04 Aug 2014 11:43:19 +0200 blanchet honor 'dont_minimize' option when preplaying one-liner proof
Sun, 22 Jun 2014 06:16:57 +0100 sultana Metis is being used to emulate E steps;
Sun, 22 Jun 2014 06:16:56 +0100 sultana updated application of print_tac to take context parameter;
Sat, 02 Aug 2014 00:15:08 +0200 blanchet better duplicate detection
Fri, 01 Aug 2014 23:58:42 +0200 blanchet normalize conjectures vs. negated conjectures when comparing terms
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip