Tue, 30 Mar 2010 00:12:42 +0200 wenzelm auto update by Netbeans 6.8;
Tue, 30 Mar 2010 00:11:41 +0200 wenzelm adapted to Netbeans 6.8 and Scala for Netbeans 6.8v1.1;
Mon, 29 Mar 2010 22:55:57 +0200 wenzelm replaced some deprecated methods;
Mon, 29 Mar 2010 22:43:56 +0200 wenzelm adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
Mon, 29 Mar 2010 01:07:01 -0700 huffman merged
Sun, 28 Mar 2010 12:50:38 -0700 huffman use lattice theorems to prove set theorems
Sun, 28 Mar 2010 12:49:14 -0700 huffman add/change some lemmas about lattices
Sun, 28 Mar 2010 10:34:02 -0700 huffman cleaned up some proofs
Mon, 29 Mar 2010 09:06:34 +0200 boehmes the configuration option 'trace_simp' now uses the reference of the ProofGeneral settings menu as (dynamic) default value
Sun, 28 Mar 2010 19:34:08 +0200 wenzelm merged
Sun, 28 Mar 2010 19:20:52 +0200 wenzelm implicit checkpoint in Local_Theory.theory as well -- no longer export Local_Theory.checkpoint;
Sun, 28 Mar 2010 18:39:27 +0200 blanchet make SML/NJ happy
Sun, 28 Mar 2010 17:43:09 +0200 wenzelm pass raw Context.generic, to avoid wasteful Context.proof_of -- Config.get_thy is often used in performance critical spots like unify.ML;
Sun, 28 Mar 2010 16:59:06 +0200 wenzelm static defaults for configuration options;
Sun, 28 Mar 2010 16:13:29 +0200 wenzelm configuration options admit dynamic default values;
Sun, 28 Mar 2010 16:29:51 +0200 wenzelm tuned;
Sun, 28 Mar 2010 15:38:07 +0200 wenzelm do not export Attrib.register_config, to make it harder to use low-level Config.declare after the bootstrap phase;
Sun, 28 Mar 2010 15:13:19 +0200 wenzelm use regular Attrib.config instead of low-level Config.declare/Attrib.register_config;
Sat, 27 Mar 2010 21:46:10 +0100 wenzelm merged
Sat, 27 Mar 2010 21:34:28 +0100 boehmes re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
Sat, 27 Mar 2010 21:38:38 +0100 wenzelm Typedef.info: separate global and local part, only the latter is transformed by morphisms;
Sat, 27 Mar 2010 18:43:11 +0100 nipkow merged
Sat, 27 Mar 2010 18:42:27 +0100 nipkow added reference to Trace Simp Depth.
Sat, 27 Mar 2010 18:12:02 +0100 wenzelm merged
Sat, 27 Mar 2010 14:48:46 +0100 Cezary Kaliszyk Automated lifting can be restricted to specific quotient types
Sat, 27 Mar 2010 18:07:21 +0100 wenzelm moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
Sat, 27 Mar 2010 17:36:32 +0100 wenzelm disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
Sat, 27 Mar 2010 16:01:45 +0100 wenzelm disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
Sat, 27 Mar 2010 15:47:57 +0100 wenzelm added Term.fold_atyps_sorts convenience;
Sat, 27 Mar 2010 15:20:31 +0100 wenzelm moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
Sat, 27 Mar 2010 14:10:37 +0100 wenzelm eliminated old-style Theory.add_defs_i;
Sat, 27 Mar 2010 02:10:00 +0100 boehmes slightly more general simproc (avoids errors of linarith)
Sat, 27 Mar 2010 00:08:39 +0100 boehmes merged
Fri, 26 Mar 2010 23:58:27 +0100 boehmes updated SMT certificates
Fri, 26 Mar 2010 23:57:35 +0100 boehmes made renamings stable under name changes in the original problem (uninterpreted names are irrelevant to the SMT solver, and caching of SMT certificates relies on irrelevancy of renamings)
Fri, 26 Mar 2010 23:46:22 +0100 boehmes replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
Fri, 26 Mar 2010 20:30:03 +0100 wenzelm merged
Fri, 26 Mar 2010 18:03:01 +0100 hoelzl Added finite measure space.
Fri, 26 Mar 2010 20:30:05 +0100 wenzelm tuned white space;
Fri, 26 Mar 2010 20:28:15 +0100 wenzelm more efficient merge_algebra for important special cases -- tricky due to required completion if class algebra changes;
Fri, 26 Mar 2010 17:59:11 +0100 wenzelm low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
Thu, 25 Mar 2010 23:18:42 +0100 wenzelm merged
Thu, 25 Mar 2010 17:56:31 +0100 blanchet merged
Thu, 25 Mar 2010 17:55:55 +0100 blanchet make Mirabelle happy again
Wed, 24 Mar 2010 14:51:36 +0100 blanchet revert debugging output that shouldn't have been submitted in the first place
Wed, 24 Mar 2010 14:49:32 +0100 blanchet added support for Sledgehammer parameters;
Wed, 24 Mar 2010 14:43:35 +0100 blanchet simplify Nitpick parameter parsing code a little bit + make compile
Wed, 24 Mar 2010 12:31:37 +0100 blanchet add new file "sledgehammer_util.ML" to setup
Wed, 24 Mar 2010 12:30:33 +0100 blanchet honor the newly introduced Sledgehammer parameters and fixed the parsing;
Tue, 23 Mar 2010 14:43:22 +0100 blanchet added a syntax for specifying facts to Sledgehammer;
Tue, 23 Mar 2010 11:40:46 +0100 blanchet leverage code now in Sledgehammer
Tue, 23 Mar 2010 11:39:21 +0100 blanchet added options to Sledgehammer;
Mon, 22 Mar 2010 15:23:18 +0100 blanchet make "sledgehammer" and "atp_minimize" improper commands
Thu, 25 Mar 2010 21:27:04 +0100 wenzelm Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
Thu, 25 Mar 2010 21:14:15 +0100 wenzelm removed unused AxClass.of_sort derivation;
Wed, 24 Mar 2010 22:30:33 +0100 wenzelm more precise dependencies;
Wed, 24 Mar 2010 22:08:03 +0100 wenzelm merged
Wed, 24 Mar 2010 17:41:25 +0100 bulwahn merged
Wed, 24 Mar 2010 17:40:44 +0100 bulwahn removed predicate_compile_core.ML from HOL-ex session
Wed, 24 Mar 2010 17:40:44 +0100 bulwahn added predicate compiler quickcheck examples to new session Predicate_Compile_Examples
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip