Tue, 22 Jun 2010 19:08:25 +0200 blanchet turn on "natural form" filtering in the Mirabelle tests, to see how it performs
Tue, 22 Jun 2010 18:47:45 +0200 blanchet missing "Unsynchronized" + make exception take a unit
Tue, 22 Jun 2010 18:31:49 +0200 blanchet added code to optionally perform fact filtering on the original (non-CNF) formulas
Tue, 22 Jun 2010 17:10:01 +0200 blanchet more cosmetics
Tue, 22 Jun 2010 17:07:39 +0200 blanchet cosmetics + prevent consideration of inlined Skolem terms in relevance filter
Tue, 22 Jun 2010 16:50:55 +0200 blanchet canonical argument order
Tue, 22 Jun 2010 16:40:36 +0200 blanchet leverage new data structure for handling "add:" and "del:"
Tue, 22 Jun 2010 16:23:29 +0200 blanchet thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
Tue, 22 Jun 2010 14:48:46 +0200 blanchet merge "generic_prover" and "generic_tptp_prover"
Tue, 22 Jun 2010 14:28:22 +0200 blanchet removed Sledgehammer's support for the DFG syntax;
Tue, 22 Jun 2010 13:17:59 +0200 blanchet distinguish between "unknown" and "no Kodkodi installed" errors
Tue, 22 Jun 2010 13:17:17 +0200 blanchet reintroduce new Sledgehammer polymorphic handling code;
Tue, 22 Jun 2010 12:19:06 +0200 blanchet make the Nitpick_Example theory processable even when Kodkodi is not installed;
Wed, 23 Jun 2010 10:05:13 +0200 hoelzl Make latex happy
Wed, 23 Jun 2010 08:44:44 +0200 Cezary Kaliszyk Quotient package now uses Partial Equivalence instead place of equivalence
Wed, 23 Jun 2010 08:42:41 +0200 Cezary Kaliszyk Replace 'list_rel' by 'list_all2'; they are equivalent.
Tue, 22 Jun 2010 19:46:16 +0200 ballarin Proper treatment of non-inherited mixins.
Tue, 22 Jun 2010 18:15:44 +0200 hoelzl merged
Mon, 21 Jun 2010 19:33:51 +0200 hoelzl Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
Tue, 22 Jun 2010 01:21:52 +0200 blanchet reredisable new polymorphic code
Mon, 21 Jun 2010 18:45:10 +0200 blanchet merged
Mon, 21 Jun 2010 18:32:16 +0200 blanchet beta-eta was too much, because it transformed SOME x. P x into Eps P, which caused problems later;
Mon, 21 Jun 2010 18:31:52 +0200 wenzelm back to post-release mode;
Mon, 21 Jun 2010 17:41:57 +0200 wenzelm merged, resolving conflicts in doc-src/IsarRef/Thy/HOL_Specific.thy;
Mon, 21 Jun 2010 16:59:37 +0200 blanchet make Nitpick's unsound mode a bit more unsound
Mon, 21 Jun 2010 14:07:00 +0200 blanchet sort cases on the proper key
Mon, 21 Jun 2010 13:35:10 +0200 blanchet compile
Mon, 21 Jun 2010 12:33:43 +0200 blanchet thread "full_types"
Mon, 21 Jun 2010 12:31:41 +0200 blanchet try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
Mon, 21 Jun 2010 12:28:46 +0200 blanchet clean up after fcc768dc9dd0
Mon, 21 Jun 2010 11:16:00 +0200 blanchet adjusted Nitpick examples to latest changes + make them slightly faster
Mon, 21 Jun 2010 11:15:21 +0200 blanchet optimized code generated for datatype cases + more;
Mon, 21 Jun 2010 09:38:20 +0200 haftmann activated Scala code generator test
Mon, 21 Jun 2010 09:38:20 +0200 haftmann added bot instances; tuned
Mon, 21 Jun 2010 09:06:14 +0200 haftmann extensionality rule fset_eqI
Sun, 20 Jun 2010 22:01:22 +0200 haftmann merged
Sun, 20 Jun 2010 19:02:41 +0200 haftmann separate section for diagnostic commands
Sat, 19 Jun 2010 09:50:30 +0200 haftmann more binding; avoid arcane Rep and Abs prefixes
Sat, 19 Jun 2010 09:14:06 +0200 haftmann cleanup of typecopy package
Sat, 19 Jun 2010 06:43:33 +0200 haftmann quickcheck for fsets
Fri, 18 Jun 2010 22:41:16 +0200 nipkow merged
Fri, 18 Jun 2010 22:40:58 +0200 nipkow added pigeonhole lemmas
Fri, 18 Jun 2010 21:22:05 +0200 haftmann merged
Fri, 18 Jun 2010 15:59:51 +0200 haftmann tuned whitespace; dropped dead code
Fri, 18 Jun 2010 15:26:04 +0200 haftmann code_simp: only succeed on real progress
Fri, 18 Jun 2010 15:26:02 +0200 haftmann prefer fold over foldl
Fri, 18 Jun 2010 15:03:21 +0200 haftmann conclude simplification with default simpset
Fri, 18 Jun 2010 15:03:21 +0200 haftmann drop subsumed default equations (requires a little bit unfortunate laziness)
Fri, 18 Jun 2010 15:03:20 +0200 haftmann avoid Scala legacy operations
Fri, 18 Jun 2010 15:03:20 +0200 haftmann prefer fold over foldl
Fri, 18 Jun 2010 09:21:41 +0200 haftmann made List.thy a join point in the theory graph
Fri, 18 Jun 2010 20:22:06 +0200 nipkow tuned set_replicate lemmas
Fri, 18 Jun 2010 14:14:42 +0200 nipkow merged
Fri, 18 Jun 2010 14:14:29 +0200 nipkow added lemmas
Fri, 18 Jun 2010 09:04:00 +0200 haftmann dropped dead code
Thu, 17 Jun 2010 19:32:05 +0200 haftmann replaced unreliable metis proof
Thu, 17 Jun 2010 16:15:15 +0200 haftmann rev is reverse in Haskell
Thu, 17 Jun 2010 15:59:48 +0200 haftmann first serious draft of a scala code generator
Thu, 17 Jun 2010 15:59:47 +0200 haftmann more precise code
Thu, 17 Jun 2010 15:59:46 +0200 haftmann explicit type variable arguments for constructors
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip