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;

more flexibile font size via CSS <style> instead of old <font> element; preformatted text;

tuned;

control tooltip font via Swing HTML, with tooltip-font-size property;

added HTML.encode (in Scala), similar to HTML.output in ML;

one extra space to accomodate symbolic indentifiers etc.;

replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information; ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information; fall back on ML_Context.eval_text if there is no position or no surrounding text; proper Args.name_source_position for method "tactic" and "raw_tactic"; tuned;

more detailed token markup, including command kind as sub_kind; type-safe access to Command.HighlightInfo;

tuned;