Sun, 30 Nov 2008 14:43:29 +0100 wenzelm tuned;
Sun, 30 Nov 2008 14:03:46 +0100 wenzelm removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
Sun, 30 Nov 2008 14:03:45 +0100 wenzelm removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
Sun, 30 Nov 2008 12:58:20 +0100 wenzelm default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
Sun, 30 Nov 2008 12:25:54 +0100 wenzelm misc tuning and clarification;
Sat, 29 Nov 2008 19:21:32 +0100 wenzelm remove repository-only files;
Sat, 29 Nov 2008 19:20:12 +0100 wenzelm more .hgignore entries;
Sat, 29 Nov 2008 19:01:28 +0100 wenzelm tuned;
Sat, 29 Nov 2008 18:26:53 +0100 wenzelm basic setup of .hgignore;
Sat, 29 Nov 2008 18:19:59 +0100 wenzelm further notes;
Sat, 29 Nov 2008 17:09:28 +0100 wenzelm Important notes on Mercurial repository access for Isabelle.
Sat, 29 Nov 2008 13:39:45 +0100 nipkow Floats for Real.
Sat, 29 Nov 2008 13:39:23 +0100 nipkow new file float_syntax.ML
Sat, 29 Nov 2008 13:37:13 +0100 nipkow New lexical item "float".
Fri, 28 Nov 2008 17:43:06 +0100 ballarin Intro_locales_tac to simplify goals involving locale predicates.
Fri, 28 Nov 2008 12:26:14 +0100 ballarin Ahere to modern naming conventions; proper treatment of internal vs external names.
Fri, 28 Nov 2008 11:55:46 +0100 kleing added Tim's find_theorems performance patch
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;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip