one all-inclusive bundle for each platform;

more robust handling of additional type variables: warning, more canonical order, drop mixfix syntax if implicit type arguments are introduced (to avoid delusion due to shifted arguments);

tuned warning;

less ambitious settings;

spelling;

do not open Proofterm, which is very ould style;

eliminated ML structure alias;

tuned default perspective;

tracing in aliceblue;

discontinued obsolete Isar.context() -- long superseded by @{context};

diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};

allow qualified names;

CONTRIBUTORS

clarified

mention unconstrain in NEWS

merged

hide default, map_entry, map_default

improved parallelism of proof term normalization;

always unconstrain thm proofs;

replaced ML pokes by explicit usedir -p; prefer -q 0 for proof terms, which avoids overhead of proof promises, while exploiting implicit parallelism of internal normalization;

merged

absolute import -- must work with Main.thy / HOL-Proofs

avoid duplicate import

HOL-Proofs is based in Main.thy

dropped lemma duplicate

msetprod_empty, msetprod_singleton

induction over non-empty lists

removed dependency of Euclid on Old_Number_Theory

modernized

removed obsolete usedir -p 1 option;

actually test smlnj;

updated keywords;

Added tag isa2009-2-test0 for changeset 935c75359742

more CONTRIBUTORS;

merged

Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs;

merged

added lemmas

merged

merge

fix parameter settings

merged

merged

update NEWS

fix Nitpick soundness bug regarding The and Eps

added examples/tests for THE and SOME

cosmetics

adapt example

fix code that used to raise an exception if bound variables were given a finite function type, because the old vs. new bound variable types were confused

improved precision of "set" based on an example from Lukas

remove debug output

removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead

subsumed by NEWS -- for older history, see previous versions of Nitpick

don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive

honor xsymbols in Nitpick

added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"

document new option

make Nitpick handle multiple typedef entries for same typedef

remove comment

thread along context instead of theory for typedef lookup

obsolete FIXME

move SAT solver warning from every invocation of SAT solver to the tool, Refute, that uses it; "size_change" rarely needs anything beyond "dpll", so this warning is annoying at best, and when "size_change" is called from Nitpick the warning confuses users, who then think that Nitpick is using "dpll" when it's really using MiniSat or some other fast solver

don't include any axioms for "TYPE" in Nitpick

dropped obsolete script

normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);

merged

avoid store flag in add_* operations

arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML; misc tuning;

merged

do not expose store flag of AxClass.add_*

merged

adapted to changes

capitalized type variables; added yield as keyword

brackify_infix etc.: no break before infix operator -- eases survival in Scala

basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short;

use local /home/isatest/polyml-5.3.0 on atbroy102 to avoid problems with the SMB filesystem via homebroy;

uniform ML environment setup for Isar and PG;

merged

Renamed TypeInfer to Type_Infer.

merged

assign now applies meet before update_new to avoid misleading error message.

Tuned.

Adapted to new format of proof terms containing explicit proofs of class membership.

classrel and arity theorems are now stored under proper name in theory. add_arity and add_classrel take extra boolean argument indicating whether theorems should be stored.

- outer_constraints with original variable names, to ensure that argsP is consistent with args - Exported map_proof_same, added implies_intr_proof' and forall_intr_proof' - Rewriting procedures used by rewrite_proof can now access hypotheses - Finally enabled unconstrain

outer_constraints with original variable names, to ensure that argsP is consistent with args

- Equality check on propositions after lookup of theorem now takes type variable renamings into account - Unconstrain theorem after lookup - Improved error messages for application cases

Use Proofterm.forall_intr_proof' instead of locally defined forall_intr_prf.

- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which all type variables have the top sort - Adapted proof_of_term to handle proofs with explicit class membership proofs

merged

merged

corrected printing of characters

corrected implementation

added Scala code setup

tuned code setup

keep structure ThyLoad for the sake of Proof General;

added random instance for word

notes on Isabelle/jEdit;

remove presently unused Isabelle application;

modernized some structure names, keeping a few legacy aliases;

merged

merge

fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option

updated generated files

clarified

adjusted

terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);

Toplevel.run_command: reraise Interrupt, to terminate the Isar_Document.execution and not store a failed attempt;

merged

Typo in locales tutorial.

Theory_Target.pretty: more markup;

tuned abbrevs for long arrows, according to usual ASCII syntax;