Fri, 28 Nov 2008 11:37:20 +0100 kleing FindTheorems performance improvements (from Timothy Bourke)
Fri, 28 Nov 2008 11:14:13 +0100 ballarin Perform higher-order pattern matching during round-up.
Thu, 27 Nov 2008 21:25:34 +0100 ballarin Proper treatment of expressions with free arguments.
Thu, 27 Nov 2008 21:25:16 +0100 ballarin Roundup bound.
Thu, 27 Nov 2008 10:30:42 +0100 ballarin Tests for sublocale command.
Thu, 27 Nov 2008 10:29:07 +0100 ballarin Sublocale command.
Thu, 27 Nov 2008 10:28:27 +0100 ballarin Command to add dependencies, fixed processing of dependencies.
Thu, 27 Nov 2008 10:26:00 +0100 ballarin Fixed strange indentation.
Tue, 25 Nov 2008 23:29:26 +0100 huffman add Algebraic and Universal to imports
Tue, 25 Nov 2008 23:29:01 +0100 huffman separate run and cases combinators
Tue, 25 Nov 2008 23:28:06 +0100 huffman renamed lemma compact_minimal to compact_bot_minimal;
Tue, 25 Nov 2008 23:26:44 +0100 huffman renamed lemma compact_minimal to compact_bot_minimal
Tue, 25 Nov 2008 18:07:33 +0100 ballarin Use standard export function.
Tue, 25 Nov 2008 18:07:01 +0100 ballarin Expression types cleaned up.
Tue, 25 Nov 2008 18:06:49 +0100 ballarin Test for term patterns added.
Tue, 25 Nov 2008 18:06:21 +0100 ballarin Expression types cleaned up, proper treatment of term patterns.
Mon, 24 Nov 2008 21:09:31 +0100 krauss check for more common errors first
Mon, 24 Nov 2008 21:00:03 +0100 krauss improved error msg; tuned
Mon, 24 Nov 2008 20:12:23 +0100 krauss removed "log" again, as IntInf.log2 already exists.
Mon, 24 Nov 2008 18:05:20 +0100 ballarin Some regression tests for theorem statements.
Mon, 24 Nov 2008 18:04:21 +0100 ballarin Enable switching to new locales during session.
Mon, 24 Nov 2008 18:03:48 +0100 ballarin Read/cert_statement for theorem statements.
Mon, 24 Nov 2008 18:02:52 +0100 ballarin Generalised activation code.
Mon, 24 Nov 2008 14:23:04 +0100 ballarin More ramifications of removal of 'includes' element.
Sun, 23 Nov 2008 18:37:56 +0100 wenzelm tuned;
Sun, 23 Nov 2008 17:27:15 +0100 wenzelm eliminated finish_proof, keep pre/post normalization of results separate;
Sun, 23 Nov 2008 17:25:56 +0100 wenzelm future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);
Fri, 21 Nov 2008 18:02:19 +0100 ballarin Regression tests for new locale implementation.
Fri, 21 Nov 2008 18:01:39 +0100 ballarin add_locale functional.
Fri, 21 Nov 2008 15:54:53 +0100 paulson Added a line that was missing from the definition
Fri, 21 Nov 2008 14:21:42 +0100 krauss added binary logarithm
Fri, 21 Nov 2008 13:17:43 +0100 paulson Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.
Fri, 21 Nov 2008 07:34:36 +0100 haftmann Name.binding
Thu, 20 Nov 2008 22:39:12 +0100 nipkow added optimizer
Thu, 20 Nov 2008 19:43:34 +0100 wenzelm reactivated some dead theories (based on hints by Mark Hillebrand);
Thu, 20 Nov 2008 19:06:05 +0100 haftmann Locale.local_note_qualified
Thu, 20 Nov 2008 19:06:03 +0100 haftmann fact table now using name bindings
Thu, 20 Nov 2008 19:06:02 +0100 haftmann dropped legacy naming code
Thu, 20 Nov 2008 14:55:28 +0100 haftmann tuned name bindings
Thu, 20 Nov 2008 14:55:25 +0100 haftmann using name bindings
Thu, 20 Nov 2008 14:51:40 +0100 haftmann name spaces and name bindings
Thu, 20 Nov 2008 10:29:35 +0100 ballarin Deleted debug message (PolyML).
Thu, 20 Nov 2008 00:03:55 +0100 wenzelm removed traces of former 'includes' element;
Thu, 20 Nov 2008 00:03:53 +0100 wenzelm updated generated files;
Thu, 20 Nov 2008 00:03:47 +0100 wenzelm Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
Wed, 19 Nov 2008 18:15:31 +0100 nipkow *** empty log message ***
Wed, 19 Nov 2008 17:55:18 +0100 nipkow fixed
Wed, 19 Nov 2008 17:54:55 +0100 nipkow Added new fold operator and renamed the old oe to fold_image.
Wed, 19 Nov 2008 17:04:29 +0100 ballarin Type inference for elements through syntax module.
Wed, 19 Nov 2008 17:03:13 +0100 ballarin Use 'if' in connection with 'is_some' and 'the'.
Wed, 19 Nov 2008 17:00:00 +0100 ballarin Basic types not qualified.
Wed, 19 Nov 2008 16:58:33 +0100 ballarin Enable switching to new locales during session.
Wed, 19 Nov 2008 08:58:57 +0100 haftmann explicit inhabitance proof
Tue, 18 Nov 2008 22:25:36 +0100 wenzelm fulfill_proof/thm_proof: commuted lazyness;
Tue, 18 Nov 2008 22:25:30 +0100 wenzelm fulfill_proof/thm_proof: commuted lazyness;
Tue, 18 Nov 2008 21:17:14 +0100 krauss removed lemmas called lemma1 and lemma2
Tue, 18 Nov 2008 18:25:59 +0100 wenzelm force_proofs after cumulative use_thys;
Tue, 18 Nov 2008 18:25:55 +0100 wenzelm signed_string_of_int for priorities;
Tue, 18 Nov 2008 18:25:52 +0100 wenzelm added force_proofs;
Tue, 18 Nov 2008 18:25:49 +0100 wenzelm added force_proofs (based on thms ever passed through enter_thms);
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip