updated web style for Mercurial 1.1.1;

misc webstyle adaptions;

updated web style for Mercurial 1.1;

removed Ids;

merged

removed Ids;

merged.

constdefs -> definition

removed Ids;

merged.

remove cvs Id tags

merged

basic setup for MacOS application bundle;

GHC ext pragma in generated Haskell modules

dropped Ids

temporary adaption to new locale code

restructured; circumvent sort problem

merged.

new theory Dsum: cpo of disjoint sum

scale dependency graph in document

changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions

proper document antiquotations;

merged

method "sizechange" proves termination of functions; added more infrastructure for termination proofs

future proofs: Future.fork_pri 1 minimizes queue length and pending promises -- slight improvement of throughput, at the cost of a bit of parallelism;

renamed structure TaskQueue to Task_Queue;

Future.fork_pri;

renamed structure TaskQueue to Task_Queue; tasks are ordered according to priority, which has been generalized from bool to int; removed unused focus; tuned dequeue: single pass due to proper priority order; tuned dequeue_towards;

renamed structure TaskQueue to Task_Queue;

renamed structure TaskQueue to Task_Queue; generalized fork_background to fork_pri; reduced tracing; map: inherit task priority; removed unused focus;

removed old scheduler;

tuned enqueue: plain add_edge, acyclic not required here;

tuned messages;

updated generated file;

repaired railroad accident;

updated generated files;

added 'atp_messages' command, which displays recent messages synchronously;

merged

flipped fold implementation

merged

codegen

code for {x:A. P(x)} and for fold

Testfile for Stefan's code generator

moved value.ML to src/Tools

\underscoreoff is now default

tuned some proofs

removed Ids;

merged

merged

merged

Unified syntax of nominal_primrec with the one used by fun(ction) and new version of primrec command.

Modified nominal_primrec to make it work with local theories, unified syntax with the one used by fun(ction) and new version of primrec command.

merged

tuned comments; tuned;

tuned ML_OPTIONS for improved multicore performance;

refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry; tuned history: renamed version to stage, disallow checkpoint/finish_thy on finished theories; added display_names -- user-level presentation; removed obsolete exists_name, names_of; tuned;

requires: check ancestors directly;

Context.display_names;

global_qed: refrain from ProofContext.auto_bind_facts, to avoid polluting the final result context with bindings involving loose free variables;

usage: echo ML settings as well;

future proofs: more robust check via Future.enabled;

removed former Isabelle font (cf. IsabelleItalic);

incorporated isabelle-fonts side-branch (forced merge);

replaced single quote by mathematical prime;

generated file;

bold version: math glyphs from plain IsabelleMono;

fixed rangle;

use dash from text font, not math;

added glyphs for \<A> (cal), \<a> (rm), \<AA> (\frak), \<aa> (frak); replaced old-style digits by bold ones (bf);

generated ttf;

renamed to IsabelleMono;

added README with original licenses;

renamed Isabelle to IsabelleItalic;

fixed rangle glyph;

the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;

Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);

Isabelle font, based on TeX glyhps;

enable future_scheduler by default;

ISABELLE_USEDIR_OPTIONS: -M max is default;

unified ids for ancestors and checkpoints, removed obsolete history of checkpoints; tuned representation of internal node names -- avoid string copies; tuned signature;

removed spurious exception_trace;

print_theorems: more robust difference, even after finished proof;

export context_node;

merged

more antiquotations;

pcpodef package: state two goals, instead of encoded conjunction;

recovered goal_pat;

inhabitance goal is now stated in original form and result contracted -- the previous attempt with contracted goal and initial unfolding did not work, because it disrupted the Isar proof structure (e.g. ?thesis);

tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.; more antiquotations; explicit Theory.requires; adapted to recent changes in ~~/src/HOL/Tools/typedef_package.ML; misc tuning and simplification;

add_typedef: unfold set_def in tactical proof as well;

merged

Theory.checkpoint before commencing proof;

misc tuning and modernisation;

merged

logically separate typedef axiomatization from constant definition

add def before setting up goal

killed dead code

constrain type inference to sort "type"

merged.

cleaned up some proofs in Cfun.thy

implement cont_proc theorem cache using theory data

use ML antiquotations

clean up diff_bin_simps

move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs

fixed import: requires ContNotDenum;

fixed import: requires ContNotDenum;

requires RComplete;

merged.

move all neg-related lemmas to NatBin; make type of neg specific to int

separate neg_simps from rel_simps

use {less,le}_number_of in integer simprocs

use lemma lists defined in Int.thy

Merged.

Satisfy a_axioms.

Merged.

Enable keyword 'structure' in for clause of locale expression.

Correct order of defines in specification.

Pass on defines in inheritance; reject illicit defines created by instantiation.

Order of implicit parameters in locale expression.

NewLocale.intro_locales_tac added to Class.default_intro_tac.

When adding locales, delay notes until local theory is built.

merged

moved ContNotDenum into Library

move lemmas from Numeral_Type.thy to other theories

instantiation option :: (enum) enum

instance inat :: semiring_char_0

Default names for definitions.

Proper shape of assumptions generated from Defines elements.

Merged.

Explicitly close up defines.

Interpretation in proof contexts.

tuned LaTeX files

tuned LaTeX files

merged.

multiplication for type inat

fix proofs

change lemmas to avoid using neg

simplify less_nat_number_of

add lemma le_nat_number_of

merged

adapted to changes in binding module

merged

Name.name_of -> Binding.base_name

corrected theory path

removed Table.extend, NameSpace.extend_table

renamed force_proof to join_proof;

renamed force_proofs to join_proofs;

finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);

improved future_schedule: more robust handling of failed parents (explicit join), final join of all futures, including Exn.release_all;

excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);

added new_task;

added constant value;

refined type deriv: replaced all_promises by max_promise (dependency limit) and open_promises (potentially unfinished/failed promises); name_thm: actually maintain max_promise/open_promises here (!), reduce open_promises as far as possible; tuned;

uniform treatment of ISABELLE_HOME/contrib vs. ISABELLE_HOME/..;

Merged.

Interpretation in theories including interaction with subclass relation.

merged

dropped NameSpace.declare_base

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

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";