consider TeX spacing conventions for punctuation marks

fix typed print translation for card UNIV

removed obsolete CVS instructions;

fixed spelling; tuned;

tuned;

removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting; separate chapter on interfaces as Isabelle tools;

removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;

default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;

misc tuning and clarification;

remove repository-only files;

more .hgignore entries;

tuned;

basic setup of .hgignore;

further notes; tuned;

Important notes on Mercurial repository access for Isabelle.

Floats for Real.

new file float_syntax.ML

New lexical item "float".

Intro_locales_tac to simplify goals involving locale predicates.

Ahere to modern naming conventions; proper treatment of internal vs external names.

added Tim's find_theorems performance patch

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.

Perform higher-order pattern matching during round-up.

Proper treatment of expressions with free arguments.

Roundup bound.

Tests for sublocale command.

Sublocale command.

Command to add dependencies, fixed processing of dependencies.

Fixed strange indentation.

add Algebraic and Universal to imports

separate run and cases combinators

renamed lemma compact_minimal to compact_bot_minimal; renamed compacts to approximants

renamed lemma compact_minimal to compact_bot_minimal

Use standard export function.

Expression types cleaned up.

Test for term patterns added.

Expression types cleaned up, proper treatment of term patterns.

check for more common errors first

improved error msg; tuned

removed "log" again, as IntInf.log2 already exists.

Some regression tests for theorem statements.

Enable switching to new locales during session.

Read/cert_statement for theorem statements.

Generalised activation code.

More ramifications of removal of 'includes' element.

tuned;

eliminated finish_proof, keep pre/post normalization of results separate;

future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);

Regression tests for new locale implementation.

add_locale functional.

Added a line that was missing from the definition

added binary logarithm

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.

Name.binding

added optimizer

reactivated some dead theories (based on hints by Mark Hillebrand);

Locale.local_note_qualified

fact table now using name bindings

dropped legacy naming code

tuned name bindings