2008-12-01 haftmann 2008-12-01 exported get_accesses (for diagnostic purpose)
2008-12-01 haftmann 2008-12-01 more means for algebra projection
2008-12-01 haftmann 2008-12-01 consider TeX spacing conventions for punctuation marks
2008-11-30 huffman 2008-11-30 fix typed print translation for card UNIV
2008-11-30 wenzelm 2008-11-30 removed obsolete CVS instructions;
2008-11-30 wenzelm 2008-11-30 fixed spelling; tuned;
2008-11-30 wenzelm 2008-11-30 tuned;
2008-11-30 wenzelm 2008-11-30 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting; separate chapter on interfaces as Isabelle tools;
2008-11-30 wenzelm 2008-11-30 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
2008-11-30 wenzelm 2008-11-30 default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
2008-11-30 wenzelm 2008-11-30 misc tuning and clarification;
2008-11-29 wenzelm 2008-11-29 remove repository-only files;
2008-11-29 wenzelm 2008-11-29 more .hgignore entries;
2008-11-29 wenzelm 2008-11-29 tuned;
2008-11-29 wenzelm 2008-11-29 basic setup of .hgignore;
2008-11-29 wenzelm 2008-11-29 further notes; tuned;
2008-11-29 wenzelm 2008-11-29 Important notes on Mercurial repository access for Isabelle.
2008-11-29 nipkow 2008-11-29 Floats for Real.
2008-11-29 nipkow 2008-11-29 new file float_syntax.ML
2008-11-29 nipkow 2008-11-29 New lexical item "float".
2008-11-28 ballarin 2008-11-28 Intro_locales_tac to simplify goals involving locale predicates.
2008-11-28 ballarin 2008-11-28 Ahere to modern naming conventions; proper treatment of internal vs external names.
2008-11-28 kleing 2008-11-28 added Tim's find_theorems performance patch
2008-11-28 kleing 2008-11-28 FindTheorems performance improvements (from Timothy Bourke) * Prefilter the list of theorems based on the constants and free variables in Pattern search terms, before calling Pattern.matches_subterm. * Apply filters successively rather than running each and then finding the intersection. * Show the time taken to run a query.
2008-11-28 ballarin 2008-11-28 Perform higher-order pattern matching during round-up.
2008-11-27 ballarin 2008-11-27 Proper treatment of expressions with free arguments.
2008-11-27 ballarin 2008-11-27 Roundup bound.
2008-11-27 ballarin 2008-11-27 Tests for sublocale command.
2008-11-27 ballarin 2008-11-27 Sublocale command.
2008-11-27 ballarin 2008-11-27 Command to add dependencies, fixed processing of dependencies.
2008-11-27 ballarin 2008-11-27 Fixed strange indentation.
2008-11-25 huffman 2008-11-25 add Algebraic and Universal to imports
2008-11-25 huffman 2008-11-25 separate run and cases combinators
2008-11-25 huffman 2008-11-25 renamed lemma compact_minimal to compact_bot_minimal; renamed compacts to approximants
2008-11-25 huffman 2008-11-25 renamed lemma compact_minimal to compact_bot_minimal
2008-11-25 ballarin 2008-11-25 Use standard export function.
2008-11-25 ballarin 2008-11-25 Expression types cleaned up.
2008-11-25 ballarin 2008-11-25 Test for term patterns added.
2008-11-25 ballarin 2008-11-25 Expression types cleaned up, proper treatment of term patterns.
2008-11-24 krauss 2008-11-24 check for more common errors first
2008-11-24 krauss 2008-11-24 improved error msg; tuned
2008-11-24 krauss 2008-11-24 removed "log" again, as IntInf.log2 already exists.
2008-11-24 ballarin 2008-11-24 Some regression tests for theorem statements.
2008-11-24 ballarin 2008-11-24 Enable switching to new locales during session.
2008-11-24 ballarin 2008-11-24 Read/cert_statement for theorem statements.
2008-11-24 ballarin 2008-11-24 Generalised activation code.
2008-11-24 ballarin 2008-11-24 More ramifications of removal of 'includes' element.
2008-11-23 wenzelm 2008-11-23 tuned;
2008-11-23 wenzelm 2008-11-23 eliminated finish_proof, keep pre/post normalization of results separate;
2008-11-23 wenzelm 2008-11-23 future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);
2008-11-21 ballarin 2008-11-21 Regression tests for new locale implementation.
2008-11-21 ballarin 2008-11-21 add_locale functional.
2008-11-21 paulson 2008-11-21 Added a line that was missing from the definition
2008-11-21 krauss 2008-11-21 added binary logarithm
2008-11-21 paulson 2008-11-21 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.
2008-11-21 haftmann 2008-11-21 Name.binding
2008-11-20 nipkow 2008-11-20 added optimizer
2008-11-20 wenzelm 2008-11-20 reactivated some dead theories (based on hints by Mark Hillebrand);
2008-11-20 haftmann 2008-11-20 Locale.local_note_qualified
2008-11-20 haftmann 2008-11-20 fact table now using name bindings