Mercurial Mercurial > repos > isabelle / shortlog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
 
Thu, 07 Aug 2014 12:17:41 +0200 blanchet generate nicer 'set' theorems for (co)datatypes changeset | files
Thu, 07 Aug 2014 12:17:41 +0200 blanchet compile changeset | files
Thu, 07 Aug 2014 12:17:41 +0200 blanchet took out test driver changeset | files
Thu, 07 Aug 2014 12:17:41 +0200 blanchet make TPTP tools work on polymorphic (TFF1) problems as well changeset | files
Thu, 07 Aug 2014 12:17:41 +0200 blanchet put comments between TPTP lines to comply with TPTP BNF changeset | files
Thu, 07 Aug 2014 12:17:41 +0200 blanchet test driver changeset | files
Thu, 07 Aug 2014 12:17:41 +0200 blanchet treat variables as frees in 'conjecture's changeset | files
Thu, 07 Aug 2014 12:17:41 +0200 blanchet support TFF1 in TPTP parser/interpreter changeset | files
Thu, 07 Aug 2014 12:17:41 +0200 blanchet tuning changeset | files
Thu, 07 Aug 2014 09:35:31 +0200 traytel tuned changeset | files
Thu, 07 Aug 2014 10:06:18 +0200 nipkow tuned changeset | files
Thu, 07 Aug 2014 09:48:04 +0200 nipkow tuned changeset | files
Wed, 06 Aug 2014 18:20:31 +0200 traytel merged changeset | files
Wed, 06 Aug 2014 16:00:11 +0200 traytel handle deep nesting in N2M changeset | files
Wed, 06 Aug 2014 10:20:50 +0200 traytel made tactic more robust changeset | files
Wed, 06 Aug 2014 18:03:43 +0200 nipkow added lemma changeset | files
Wed, 06 Aug 2014 08:18:35 +0200 nipkow replaced misleading - by _ changeset | files
Tue, 05 Aug 2014 20:25:12 +0200 blanchet more correct clique computation for N2M changeset | files
Tue, 05 Aug 2014 15:55:39 +0200 blanchet regenerated ML-Lex/Yacc files changeset | files
Tue, 05 Aug 2014 15:54:47 +0200 blanchet correctly interpret arithmetic types changeset | files
Tue, 05 Aug 2014 14:02:47 +0200 blanchet added 'datatype_compat' tests changeset | files
Tue, 05 Aug 2014 13:52:35 +0200 blanchet tuning whitespace changeset | files
Tue, 05 Aug 2014 11:07:53 +0200 blanchet tuned skolemization changeset | files
Tue, 05 Aug 2014 10:59:40 +0200 blanchet rationalize Skolem names changeset | files
Tue, 05 Aug 2014 10:17:15 +0200 blanchet tuning changeset | files
Tue, 05 Aug 2014 10:02:35 +0200 blanchet tuned code changeset | files
Tue, 05 Aug 2014 09:58:23 +0200 blanchet don't rename variables which will be renamed later anyway changeset | files
Tue, 05 Aug 2014 09:55:42 +0200 blanchet normalize skolem argument variable names so that they coincide when taking the conjunction changeset | files
Tue, 05 Aug 2014 09:20:00 +0200 blanchet tuning changeset | files
Mon, 04 Aug 2014 16:55:03 +0200 blanchet tuned comments changeset | files
Mon, 04 Aug 2014 16:53:09 +0200 blanchet deal with E definitions changeset | files
Mon, 04 Aug 2014 15:08:13 +0200 blanchet updated 'compress' docs changeset | files
Mon, 04 Aug 2014 15:02:02 +0200 blanchet cleaner 'compress' option changeset | files
Mon, 04 Aug 2014 14:19:43 +0200 blanchet renamed 'sh_minimize' to 'minimize'; compile; changeset | files
Mon, 04 Aug 2014 13:48:05 +0200 blanchet restored more sorting changeset | files
Mon, 04 Aug 2014 13:16:18 +0200 blanchet tuned terminology (cf. 'isar_proofs' option) changeset | files
Mon, 04 Aug 2014 13:13:10 +0200 blanchet sort facts in minimizer as well changeset | files
Mon, 04 Aug 2014 13:06:24 +0200 blanchet default on 'metis' for ATPs if preplaying is disabled changeset | files
Mon, 04 Aug 2014 12:52:48 +0200 blanchet more informative preplay failures changeset | files
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 changeset | files
Mon, 04 Aug 2014 11:54:23 +0200 blanchet slightly earlier exit from preplaying changeset | files
Mon, 04 Aug 2014 11:43:19 +0200 blanchet honor 'dont_minimize' option when preplaying one-liner proof changeset | files
Sun, 22 Jun 2014 06:16:57 +0100 sultana Metis is being used to emulate E steps; changeset | files
Sun, 22 Jun 2014 06:16:56 +0100 sultana updated application of print_tac to take context parameter; changeset | files
Sat, 02 Aug 2014 00:15:08 +0200 blanchet better duplicate detection changeset | files
Fri, 01 Aug 2014 23:58:42 +0200 blanchet normalize conjectures vs. negated conjectures when comparing terms changeset | files
Fri, 01 Aug 2014 23:33:43 +0200 blanchet tweaked 'clone' formula detection changeset | files
Fri, 01 Aug 2014 23:29:50 +0200 blanchet fine-tuned Isar reconstruction, esp. boolean simplifications changeset | files
Fri, 01 Aug 2014 23:29:49 +0200 blanchet centralized boolean simplification so that e.g. LEO-II benefits from it changeset | files
Fri, 01 Aug 2014 20:44:51 +0200 blanchet careful when compressing 'obtains' changeset | files
Fri, 01 Aug 2014 20:44:29 +0200 blanchet better handling of variable names changeset | files
Fri, 01 Aug 2014 20:15:41 +0200 blanchet try to get rid of skolems first changeset | files
Fri, 01 Aug 2014 20:08:50 +0200 blanchet nicer generated variable names changeset | files
Fri, 01 Aug 2014 19:44:18 +0200 blanchet tuning changeset | files
Fri, 01 Aug 2014 19:36:23 +0200 blanchet tuning changeset | files
Fri, 01 Aug 2014 19:32:46 +0200 blanchet no need to 'obtain' variables not in formula changeset | files
Fri, 01 Aug 2014 19:32:10 +0200 blanchet more precise handling of LEO-II skolemization changeset | files
Fri, 01 Aug 2014 16:07:34 +0200 blanchet beware of 'skolem' rules that do not skolemize (e.g. LEO-II) changeset | files
Fri, 01 Aug 2014 16:07:33 +0200 blanchet tuning changeset | files
Fri, 01 Aug 2014 16:07:33 +0200 blanchet peek instead of joining -- is perhaps less risky changeset | files
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip
isabelle