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
Wed, 24 Mar 2010 17:40:44 +0100 bulwahn adopting examples to Library move
Wed, 24 Mar 2010 17:40:43 +0100 bulwahn moved further predicate compile files to HOL-Library
Wed, 24 Mar 2010 17:40:43 +0100 bulwahn added simple setup for arithmetic on natural numbers
Wed, 24 Mar 2010 17:40:43 +0100 bulwahn removing uncommented examples in setup theory of predicate compile quickcheck
Wed, 24 Mar 2010 17:40:43 +0100 bulwahn moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
Wed, 24 Mar 2010 21:55:30 +0100 wenzelm slightly more logical bootstrap order -- also helps to sort out proof terms extension;
Wed, 24 Mar 2010 07:50:21 -0700 huffman remove ancient continuity tactic
Wed, 24 Mar 2010 15:21:42 +0100 boehmes removed Cache_IO component
Wed, 24 Mar 2010 14:08:07 +0100 boehmes updated SMT certificates
Wed, 24 Mar 2010 14:03:52 +0100 boehmes inhibit invokation of external SMT solver
Wed, 24 Mar 2010 12:30:21 +0100 boehmes more precise dependencies
Wed, 24 Mar 2010 09:44:47 +0100 boehmes cache_io is now just a single ML file instead of a component
Wed, 24 Mar 2010 09:43:34 +0100 boehmes use internal SHA1 digest implementation for generating hash keys
Wed, 24 Mar 2010 08:22:43 +0100 boehmes remove component Cache_IO (external dependency on MD5 will be replaced by internal SHA1 digest implementation)
Tue, 23 Mar 2010 19:03:05 -0700 huffman merged
Tue, 23 Mar 2010 13:42:12 -0700 huffman minimize dependencies
Tue, 23 Mar 2010 12:20:27 -0700 huffman sublocale comm_monoid_add < setprod --> sublocale comm_monoid_mult < setprod
Tue, 23 Mar 2010 22:43:53 +0100 boehmes use ml_platform instead of ml_system to distinguish library names
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip