slightly faster default compilation of Isabelle/Scala;

more explicit last exec result;

dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result; discontinued odd "touched" field -- check given edits directly;

tuned;

simplified Future.cancel/cancel_group (again) -- running threads only; more robust update/cancel_execution: full join_tasks of group before exec state assignment; tuned signature;

added ML pretty-printing;

merged

merged

explicit constructor Nat leaves nat_of as conversion

abandoned almost redundant *_foldr lemmas

tuned

no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code

enable parallel proofs (cf. e8552cba702d), only affects packages so far; disable quick_and_dirty to make packages produce proofs -- NB: 'sorry' works via "int" mode of proof commands;

added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);

tuned proofs;

more robust update_perspective, e.g. required after reload of buffer that is not at start position;

tuned imports;

updated header keywords;

init message not bad;

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;

discontinued obsolete last_execs (cf. cd3ab7625519);

remove now-unnecessary type annotations from lift_definition commands

more robust generation of quotient rules using tactics

merged

add function dest_Quotient

standardized alias;

fixed document;

merged

correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should

detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr

make Quotient_Def.lift_raw_const working again

use standard quotient lemmas to generate transfer rules

add transfer lemmas for quotients

define reflp directly, in the manner of symp and transp

set up and use lift_definition for word operations

lift_definition declares transfer_rule attribute

configure transfer method for 'a word -> int

added timestamps to logging of named thms

merged

merged

add lemmas for generating transfer rules for typedefs

tuned;

improved import_tptp to use standard TPTP directory structure; extended the TPTP testing theory to include an example of using the import_tptp command;

merge

HOL/Import more precise map types

HOL/Import typed matches against Isabelle typedef result

connect the Quotient package to the Lifting package

support non-open typedefs; define cr_rel in terms of a rep function for typedefs

tuned;

added interpretation for formula conditional;

refactored tptp lex;

refactored tptp yacc to bring close to official spec;

transfer method generalizes over free variables in goal

add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer

update keywords file

merged

fix typos

lift_definition command generates transfer rule

prove_quot_theorem fixes types

documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS

added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck; added examples of quickcheck_locale option; trying to speed up Quickcheck_Examples;

stop node execution at first unassigned exec;

discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;

more scalable execute/update: avoid redundant traversal of invisible/finished nodes; tuned;

less ambitious memo_eval, since memo_result is still not robust here;

less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;

more explicit memo_eval vs. memo_result, to enforce bottom-up execution; edit of perspective touches node superficially, to ensure revisit after update;

Command.memo including physical interrupts (unlike Lazy.lazy); re-assign unstable exec, i.e. reset interrupted transaction; node result as direct exec -- avoid potential interrupt instability of Lazy.map;

tuned;

tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;

proper signature constraint;

tuned comments;

separate module for prover command execution;

tuned;

fix typo in ML structure name

removed obsolete isar-overview manual;

dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret

merged

rudimentary handling of products in finitize_functions in Quickcheck-Narrowing

improved equality check for modes in predicate compiler

rename ML structure to avoid shadowing earlier name

add type annotations to make SML happy (cf. ec6187036495)

merged

new transfer proof method

renamed Tools/transfer.ML to Tools/legacy_transfer.ML

prefer prog-prove, suppress isar-overview;

merged

merged

formal integration of "prog-prove" manual; "main" is a reference manual;

prefer static dependencies;

merged

modernized obsolete old-style theory name with proper new-style underscore

removed use of CharVector in generated parser, to make SMLNJ happy

avoid duplicate PIDE markup; tuned;

less intrusive visibility;

more robust re-import wrt. non-HHF assumptions;

consider polyml-5.3.0 as "experimental" since it chokes on HOL-Codegenerator_Test, while 5.2.1 happens to work;

close context elements via Expression.cert/read_declaration; ensure visible context;

merged

added me to isatest email list

new package Lifting - initial commit

add floor/ceiling lemmas suggested by René Thiemann

made sure that " is shown in tutorial text

merged

tuned proofs

merged

towards showing " in the tutorial

tuned proof in order to avoid warning message

remove unnecessary qualifiers on names

add lemma Suc_1

merged

Require "For" keyword to be followed by at least one whitespace, to avoid that identifiers starting with "For" are interpreted as traceability information

normalize defs (again, cf. 008b7858f3c0);

some context examples;

retain literal non-HHF assumptions, to facilitate re-import in Generic_Target.import_export_proof;

another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);

export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);

better drop background syntax if entity depends on parameters; more direct Type_Infer_Context.const_type instead of Syntax.check_term, which expands abbreviations (and potentially more);

more uniform abbrev vs. define;

tuned;