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

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

using name bindings

name spaces and name bindings

Deleted debug message (PolyML).

removed traces of former 'includes' element;

updated generated files;

Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;

*** empty log message ***

fixed

Added new fold operator and renamed the old oe to fold_image.

Type inference for elements through syntax module.

Use 'if' in connection with 'is_some' and 'the'.

Basic types not qualified.

Enable switching to new locales during session.

explicit inhabitance proof

fulfill_proof/thm_proof: commuted lazyness; join_futures: Exn.release_all is back again (still required for implicit join of Toplevel.excursion);

fulfill_proof/thm_proof: commuted lazyness;

removed lemmas called lemma1 and lemma2

force_proofs after cumulative use_thys; PureThy.force_proofs;

signed_string_of_int for priorities; tuned;

added force_proofs; join_futures: no errors here;

added force_proofs (based on thms ever passed through enter_thms);

tuned;

eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion; eliminated obsolete alias rewtac for rewrite_goals_tac;

moved table of standard Isabelle symbols to isar-ref manual;

added isabelle-implementation manual;

disabled threads -- as advertized;

changes by Fabian Immler: improved handling of prover errors; explicit treatment of clauses that are too trivial for resolution;

Code for switching to new locales.

add_thmss

Activate elements moved to element.ML.

finish: force proofs;

finish_proof: undefined promises may occur here;

tuned promise/fullfill;

unified treatment of PAxm/Oracle/Promise in basic proof term operations; refined promise/fulfill: maintain proper type instantiation, disallow term variables; thm_proof: uniform finish_proof before and after fulfill;

removed Induct/Mutil.thy -- the file has been moved to AFP;

simplified thm_deps -- no need to build a graph datastructure;

removed Induct/Mutil.thy -- the file has been moved to AFP;

-> AFP

tuned unfold_locales invocation

explicit name morphism function for locale interpretation

Name.name_with_prefix (temporarily)

adjusted locale signature to *_cmd convention

whitespace tuning

Generic activation of locales.

proof_body/pthm: removed redundant types field;

put_name/thm_proof: promises are filled with fulfilled proofs; tuned;

proof_body/pthm: removed redundant types field; fold_proof_atoms: unified recursive case with fold_body_thms; tuned signature;

clarified Thm.proof_body_of vs. Thm.proof_of;

- Corrected order of quantification over Frees. - Fixed bug in handling of TFrees that caused variable order to get mixed up.

Frees in PThms are now quantified in the order of their appearance in the proposition as well, to make it compatible (again) with variable order used by forall_intr_frees.

adapted PThm and MinProof;

retrieve thm deps from proof_body; removed obsolete enable/disable operation;

retrieve thm deps from proof_body;

adapted PThm;

proof_of_term: removed obsolete disambiguisation table; adapted PThm; Thm.proof_of returns proof_body;

rewrite_proof: simplified simprocs (no name required); adapted PThm; fold_proof_atoms;

Thm.proof_of returns proof_body; adapted PThm;

refined notion of derivation, consiting of promises and proof_body; removed oracle_of (would require detailed check wrt. promises); proof_of returns proof_body;

reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial); added type proof_body, which covers oracles and thms of local proof; added general fold_body_thms, fold_proof_atoms; removed thms_of_proof, thms_of_proof', axms_of_proof; slightly more abstract handling of body content (oracles, thms); rewrite_proof: simplified simprocs (no name required); thm_proof: lazy fulfillment of promises;

pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);

ProofSyntax.proof_of_term: removed obsolete disambiguisation table; adapted PThm;

name_of_thm: Proofterm.fold_proof_atoms; Thm.proof_of returns proof_body;

Thm.proof_of returns proof_body;

clean: added HOL-Main;

rewrite_proof: simplified simprocs (no name required);

multithreading support for polyml-5.2 actually disabled -- as advertized;

Initial part of locale reimplementation.

Made local_note_prefix public.

re-educated guess

namify and name_decl combinators

Name.is_nothing

lemmas about dom and minus / insert

added length_unique operation for code generation

updated generated files;

removed "includes" element (lost update?);

updated generated files;

added section "Explicit instantiation within a subgoal context";

renamed "Rules" to "Object-level rules";

more on basic tactics;

basic ML reference for tactics;

added section "Tactics";

more contributors;

separate section "Inspecting the syntax" for print_syntax;

misc tuning of inner syntax;

added inner lexical syntax, reusing outer one;

misc tuning;

tuned outer lexical syntax; fixed var/tvar: really need question marks here;

more tuning of Pure grammer;

updated and elaborated Pure grammer;

added Pure grammer (from old ref manual);

mixfix annotations: verbatim for special symbols;

added section "The Pure grammar" (incomplete version, based on old ref manual);

added section "Priority grammars" (variant from old ref manual);

added section "Co-regularity of type classes and arities" (variant from old ref manual); tuned arity spacing;

minor tuning (according to old ref manual);

misc tuning and rearrangement of section "Printing logical entities";

misc tuning and rearrangement of section "Printing logical entities";

fixed/tuned syntax for attribute "tagged";

added pretty printing options (from old ref manual);

separate chapter "Inner syntax --- the term language";

updated/refined types of Isar language elements, removed special LaTeX macros;

unified use of declaration environment with IsarImplementation; tuned ML decls;

ignore ThyOutput.source flag;

added bind_thm, bind_thms;

tuned section "Incorporating ML code"; moved method_setup to separate section "Defining proof methods";

tuned section "Oracles";

tuned section arrangement;

moved section "Proof method expressions" to proof chapter; minor rearrangement of proof sections;

more on mixfix annotations (updated material from old ref manual);

tuned;

moved section "Document preparation" to front;

updated section "Markup via command tags";

renamed "formal comments" to "document comments"; tuned section "Markup commands"; updated/tuned section "Document Antiquotations";

renamed "formal comments" to "document comments";

tuned "Markup commands";

tuned intro of "Document preparation";

reworked "Defining Theories";

removed Assert.thy

dropped superfluos eval_conv

moved assert to Heap_Monad.thy

simproc for let

improved handling of !!/==> for eval and normalization

proper name morphisms for locales

consider prefixes for name bindings of simprocs (a first approximation)

diagnostic output for name bindings

Some modifications in code for proving arities to make it work for datatype definitions with additional sort constraints.

min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf

restruced naming code in anticipation of introduction of name morphisms

more verbose element printing

clarified comment

Added support for parametric datatypes.

Streamlined functions for accessing information about atoms.

Some more functions for accessing information about atoms.

Made doc compatible with the system.

clarified verbatim vs. typewriter

using explicit interpretaton prefix in Name.binding (still on the surface)

explicit interpretation prefix in Name.binding

tuned

exported codegen_preproc

Minor cleanup.

Keyword 'includes' gone.

tuned

added lemma

Added second tiling example.

cleaned

tuned

class morphism stemming from locale interpretation

improved verbatim mechanism

Theorem "_" is now stored with open derivation.

Removed argument prf2 in rewrite rules for equal_elim to make them applicable to eta-contracted proofs.

Replaced arbitrary by undefined.

Dropped context element 'includes'.