Tue, 02 Jun 2015 13:55:43 +0200 wenzelm clarified context;
Tue, 02 Jun 2015 11:03:02 +0200 wenzelm clarified context;
Tue, 02 Jun 2015 10:12:46 +0200 wenzelm clarified context;
Tue, 02 Jun 2015 10:12:29 +0200 wenzelm clarified context;
Tue, 02 Jun 2015 09:40:04 +0200 wenzelm clarified context;
Tue, 02 Jun 2015 09:16:19 +0200 wenzelm clarified context;
Tue, 02 Jun 2015 09:10:05 +0200 wenzelm tuned proof;
Wed, 03 Jun 2015 09:32:49 +0200 noschinl merged
Tue, 02 Jun 2015 13:14:36 +0200 noschinl simps_of_case: Better error if split rule is not an equality
Tue, 02 Jun 2015 13:14:11 +0200 noschinl simps_of_case: allow Drule.dummy_thm as ignored split rule
Mon, 01 Jun 2015 18:59:22 +0200 haftmann implicit partial divison operation in integral domains
Mon, 01 Jun 2015 18:59:21 +0200 haftmann separate class for division operator, with particular syntax added in more specific classes
Mon, 01 Jun 2015 18:59:21 +0200 haftmann explicit check for field sort, to anticipate situation where syntactic checking alone will not be sufficient any longer
Mon, 01 Jun 2015 18:59:21 +0200 haftmann dropped dead config option
Mon, 01 Jun 2015 18:59:20 +0200 haftmann tuned, including proper signature for functor argument
Mon, 01 Jun 2015 18:59:20 +0200 haftmann dropped dead code
Mon, 01 Jun 2015 18:59:20 +0200 haftmann explicit argument expansion of uncheck rules;
Mon, 01 Jun 2015 18:59:20 +0200 haftmann explicit input marker for operations
Mon, 01 Jun 2015 18:59:20 +0200 haftmann completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
Mon, 01 Jun 2015 18:59:20 +0200 haftmann self-contained formulation of abbrev for named targets
Mon, 01 Jun 2015 18:59:20 +0200 haftmann correct sort constraints for abbreviations in type classes
Mon, 01 Jun 2015 18:59:20 +0200 haftmann separate function to compute exported abbreviation
Mon, 01 Jun 2015 18:59:20 +0200 haftmann clearly separated target primitives (target_foo) from self-contained target operations (foo)
Mon, 01 Jun 2015 18:59:20 +0200 haftmann tuned order
Mon, 01 Jun 2015 18:59:20 +0200 haftmann dedicated config options to deactivate uncheck phase for improvable syntax
Mon, 01 Jun 2015 18:59:19 +0200 haftmann clarified interfaces for improvable syntax
Mon, 01 Jun 2015 18:59:19 +0200 haftmann tuned
Mon, 01 Jun 2015 18:07:36 +0200 wenzelm clarified context;
Mon, 01 Jun 2015 17:44:45 +0200 wenzelm clarified context;
Mon, 01 Jun 2015 17:08:47 +0200 wenzelm clarified context;
Mon, 01 Jun 2015 16:07:38 +0200 wenzelm tuned;
Mon, 01 Jun 2015 15:39:53 +0200 wenzelm discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction;
Mon, 01 Jun 2015 15:06:09 +0200 wenzelm discontinued legacy;
Mon, 01 Jun 2015 13:52:35 +0200 wenzelm obsolete (see 189c81779a68);
Mon, 01 Jun 2015 13:46:23 +0200 wenzelm eliminated odd C combinator -- Isabelle/ML usually has canonical argument order;
Mon, 01 Jun 2015 13:35:16 +0200 wenzelm clarified context;
Mon, 01 Jun 2015 13:32:36 +0200 wenzelm clarified context;
Mon, 01 Jun 2015 11:47:25 +0200 wenzelm tuned;
Mon, 01 Jun 2015 11:46:03 +0200 wenzelm clarified context;
Mon, 01 Jun 2015 10:47:08 +0200 wenzelm tuned;
Sun, 31 May 2015 00:20:35 +0200 wenzelm obsolete;
Sun, 31 May 2015 00:17:47 +0200 wenzelm clarified context;
Sun, 31 May 2015 00:16:26 +0200 wenzelm tuned;
Sun, 31 May 2015 00:11:12 +0200 wenzelm tuned;
Sat, 30 May 2015 23:58:06 +0200 wenzelm standardize towards Thm.eta_long_conversion, which just does eta_long conversion;
Sat, 30 May 2015 23:30:54 +0200 wenzelm tuned spelling;
Sat, 30 May 2015 22:18:12 +0200 wenzelm unused;
Sat, 30 May 2015 22:04:15 +0200 wenzelm tuned;
Sat, 30 May 2015 21:52:37 +0200 wenzelm more explicit context;
Sat, 30 May 2015 21:28:01 +0200 wenzelm obsolete;
Sat, 30 May 2015 20:21:53 +0200 wenzelm tuned -- more direct Thm.renamed_prop;
Sat, 30 May 2015 19:29:21 +0200 wenzelm tuned message;
Sat, 30 May 2015 19:28:51 +0200 wenzelm tuned whitespace;
Fri, 29 May 2015 17:56:43 +0200 blanchet removed model checks from Nitpick
Fri, 29 May 2015 17:17:50 +0200 blanchet document Nitpick issue
Fri, 29 May 2015 14:35:59 +0100 paulson uncountability: open interval equivalences
Thu, 28 May 2015 14:33:35 +0100 paulson Convex hulls: theorems about interior, etc. And a few simple lemmas.
Thu, 28 May 2015 10:18:46 +0200 blanchet made Auto Sledgehammer behave more like the real thing
Thu, 28 May 2015 09:50:17 +0200 blanchet took out Sledgehammer minimizer optimization that breaks things
Thu, 28 May 2015 17:25:57 +1000 kleing modernized (slightly) type compiler in MicroJava
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip