fix proofs

merged.

revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)

remove duplicated lemmas

include iszero_simps in lemmas comp_arith

add named lemma lists: neg_simps and iszero_simps

change arith_special simps to avoid using neg

merged

run test for sunbroy2 on /tmp, be careful about removing old test dir

merged

refined Future.fork interfaces, no longer export Future.future;

fork/map: no inheritance of group (structure is nested, not parallel); removed group thread_data; refined Future.fork interfaces, no longer export Future.future;

future proofs: pass actual futures to facilitate composite computations; removed join_futures -- superceded by higher-level PureThy.force_proofs;

renamed type Lazy.T to lazy; force_proofs: original order;

future_scheduler: no global task group, exceptions via collective join; finish: removed PureThy.force_proofs, back to old version;

renamed type Lazy.T to lazy; renamed type Future.T to future;

excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;

future proofs: pass actual futures to facilitate composite computations;

renamed type Future.T to future; added map combinator;

renamed type Lazy.T to lazy;

merged.

change more lemmas to avoid using iszero

change some lemmas to avoid using iszero

enable eq_bin_simps for simplifying equalities on numerals

merged

cleaned up binding module and related code

NEWS

fix proofs related to simplification of inequalities on numerals

enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals

simplify proof of less_nat_number_of

merged.

fixed proofs due to changes in Int.thy

cleaned up subsection headings; added simp rules for comparisons on binary numbers

sources are not executable;

eliminated traces of old Distribution directory;

merged

remove *.lof as well;

merged

made repository layout more coherent with logical distribution structure; stripped some $Id$s

Sublocale: removed public after_qed; identifiers private to NewLocale.

Made global_note_qualified public.

more examples

fixed typo

unfold_locales is default method - no need for explicit references

Automated merge with file:///mnt/home/isabelle-repository/repos/isabelle

Corrected imports.

clean up imports related to ContNotDenum

ignore aux stuff in doc-src;

merged

new Binding module

Locale.*note* with conventional argument type

added code equation for subset

Merged again.

Merged.

No resolution of patterns within context statements.

removed CVS Id;

proper check of ISABELLE_TOOLS directories;

removed obsolete tags (leftover from old CVS branches);

makedist -- make Isabelle source distribution (Mercurial version);

renamed makedist_mercurial to makedist, deleting the old version;

updated to python2.5;

convert to isabelle-cvs, the old version;

adapted description: old CVS;

Methods intro_locales and unfold_locales apply to both old and new locales.

code_include with attach

experimental implementation of a well-sorting algorithm

code_funcgr interface includes also sort algebra

exported get_accesses (for diagnostic purpose)

more means for algebra projection

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