proper grounding of free types produced by reconstruct_proof/infer_type, e.g. relevant for Lattices_Big.semilattice_set.infinite;

tuned;

tuned whitespace;

clarified;

tuned signature;

more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;

uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with export_proofs of re-used nodes;

more robust expose_proofs corresponding to register_proofs/consolidate_theory;
expose_proofs of class algebra more aggresively, to ensure early export within original theory/session context;

clarified signature -- more options;

proper graph traversal -- avoid exponential blowup (amending 71d1971d67ad);

more scalable protocol_message: use XML.body directly (Output.output hook is not required);

clarified signature;

clarified signature (again);

clarified signature;

make double-sure that internal proof boxes are exported, e.g. in Pure;

clarified modules (again);

more detailed proof term output;
tuned signature;

tuned signature;

more accurate proof_boxes -- from actual proof body;

proper order of variables, independently of varify/unvarify state -- relevant for export of locale conclusions;

clarified signature: name of standard_proof is authentic, otherwise empty;

clarified expand_proof/expand_name: allow more detailed control via thm_header;
export_standard_proofs: authentic theorem names in "print" format;

export toplevel proof similar to named PThm;

tuned signature;

turn hidden terms into dummy, e.g. relevant for boundary cases of reconstruct_proof;

proof boxes based on proof digest (not proof term): thus it works with prune_proofs;

clarified proof_boxes (requires prune_proofs=false);

more robust: avoid looping Lazy.force due to misinterpreted interrupt;

more informative combination_proof, e.g. relevant for proper type inference in HOL.Product_Type (with export_proofs);

tuned -- more stable type inference;

more support for proof terms;
clarified signature;

clarified proof export;

skip (somewhat pointless) shrink_proof more uniformly;

apply_preproc for all proof boxes;

support preprocessing of exported proofs;

more compact XML;

more compact XML: separate environment for free variables;
clarified fold_proof_terms vs. fold_proof_terms_types;

clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;

proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;

clarified oracle_proof;

tuned;

tuned;

tuned;

clarified signature;

tuned signature;

proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);

clarified modules;

tuned whitespace;

more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;

tuned;

misc tuning and clarification;

clarified signature -- some operations to support fully explicit proof terms;

tuned;

tuned;

proper treatment of sorts;

tuned app_types: more direct map_proof_types_same;

Term_XML.Encode/Decode.term uses Const "typargs";

more compact: avoid pointless PThm rudiments;

clarified signature: prefer total operations;

clarified thm_id vs. thm_node/thm: retain theory_name;
support for thm_deps: expand unnamed nodes;

tuned;

tuned;

tuned signature;

clarified modules;

clarified modules;

tuned;

clarified signature;

tuned signature;

back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;

tuned;

discontinued peek_status: unused and not clearly defined;

more robust, notably for open_proof of unnamed derivation;

clarified type for recorded oracles;

clarified signature;

clarified signature;

clarified identity of PThm nodes: do not reuse old id after renaming -- enforce uniqueness of substructures;

more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration;

more careful treatment of standard_vars: rename apart from existing frees and avoid approximative Name.declared, proper application of unvarifyT within terms of proof;

clarified PThm: theory_name simplifies retrieval from exports;

export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;

clarified name context for abstractions -- in contrast to 367e60d9aa1b and Term.variant_frees (*as they are printed :-*);

tuned;

uniform standard_vars for terms and proof terms;

tuned -- eliminated unused parameters;

more direct/compact export of proof terms;

more careful export of unnamed proof boxes: avoid duplicates via memoing;

tuned signature;

export each PThm node separately: slightly more scalable;

more positions;

tuned;

formal position for PThm nodes;

clarified ML types;

proper treatment of body oracles, outside of recursion into thms graph;

more direct proofs for type classes;
misc tuning and cleanup;

clarified module structure;

clarified export: retain proof boxes as local definitions -- more scalable;

clarified global theory context;

more robust export, based on reconstruct_proof / expand_proof;

clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;

discontinue clean_proof: without type args its PThm nodes are not expanded, but with type args it is too unstable;

more diagnostic operations;

tuned -- non-strict args;

tuned signature;

clarified signature;
tuned;

tuned signature;

tuned;

tuned;

tuned -- reorder sections;

tuned;

tuned signature;

tuned;

finalize proofs earlier to reduce memory requirement;

more explicit type proof_serial;

defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement;
misc tuning and clarification;

prefer local counter;

more accurate proof export;

tuned;

more thorough clean_proof;

treat MinProof like Promise before 725438ceae7c, e.g. relevant for performance of session Corec (due to Thm.derivation_closed/close_derivation);

clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named;
added Proofterm.clean_proof as simplified version of Reconstruct.expand_proof;

tuned comments;

proof terms are always constructed sequentially;
discontinued unused Proofterm.Promise -- too complex;

tuned comments -- proper sections;

support export_proofs, prune_proofs;
tuned comments;

clarified postproc: apply shrink_proof last, e.g. relevant for export of full proof term;

tuned;

clarified exception;

tuned;

more accurate type information;

global declaration of abstract syntax for proof terms, with qualified names;
clarified modules;

tuned -- slightly smaller future closure size;

more ambitious parallelism (in contrast to a8ee8e4884ec): pri = 1 ensures that internal proof tasks are executed before the already forked theory outline with pri = 0;

less ambitious parallelism: avoid problems with HOL-Proofs and threads=2 (congestion with many thousands futures and rather dense heap);

tuned: more parallel;

consolidate proofs more simultaneously;

more informative task_statistics;

tuned signature -- prefer qualified names;

consolidate nested thms with persistent result, for improved performance;
always consolidate parts of fulfill_norm_proof: important to exhibit cyclic thms (via non-termination as officially published), but this was lost in f33d5a00c25d;

tuned signature -- more abstract type thm_node;

tuned signature;

more careful derivation_closed / close_derivation;

tuned whitespace;

tuned -- fewer warnings;

tuned signature;

prefer regular context update, to allow continuous editing of Pure;

provide explicit hint concering uniqueness of derivation

local fixes may depend on goal params;

renamed "pairself" to "apply2", in accordance to @{apply 2};

more qualified names;

immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;

backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;

manage option "proofs" within theory context -- with minor overhead for primitive inferences;

support for XML data representation of proof terms;

tuned signature;
tuned comments;

discontinued home-made sharing for proof terms -- leave memory management to the Poly/ML RTS;

avoid extra fork for fulfill_proof_future whenever possible -- without proof terms it merely doubles the number of proof tasks redundantly, by piggy-backing another 10 microseconds task;

no fork from draft thy -- avoid potential for crash via classrel_proof/arity_proof;

theorem status about oracles/futures is no longer printed by default;
renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics;

added Term.dummy_pattern conveniences;

more direct balanced version Ord_List.unions;

reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;

tuned future priorities (again);

clarified fulfill_norm_proof: no join_thms yet;
clarified priority of fulfill_proof_future, which is followed by explicit join_thms;
explicit Thm.future_body_of without join yet;
tuned Thm.future_result: join_promises without fulfill_norm_proof;

added Future.joins convenience;
clarified Future.map: based on Future.cond_forks;

incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof -- avoid full graph traversal of former Proofterm.join_bodies;

tuned;

avoid OldTerm operations -- with subtle changes of semantics;

avoid OldTerm operations -- with subtle changes of semantics;

future_job: explicit indication of interrupts;

misc tuning and clarification;

tuned whitespace;

recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;

tuned signature -- corresponding to Scala version;

tuned signature: Name.invent and Name.invent_names;

simplified Name.variant -- discontinued builtin fold_map;

discontinued Name.variant to emphasize that this is old-style / indirect;

more robust exception pattern General.Subscript;

tuned comments;

clarified Proofterm.proofs_enabled;

tuned signature;
tuned vacous forks;

support named tasks, for improved tracing;

more direct Future.bulk, which potentially reduces overhead for Par_List;
tuned signature;

modernized structure Ord_List;

replaced Table.map' by Table.map

always unconstrain thm proofs;

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

- 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

modernized some structure names, keeping a few legacy aliases;

added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;

conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;

avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;

raise Fail uniformly for proofterm errors, which appear to be rather low-level;

unconstrainT operations on proofs, according to krauss/schropp;

added Proofterm.get_name variants according to krauss/schropp;
tuned signature;

tuned signature;

added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;

back-patching of axclass proofs;

strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;

proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
* present type variables are only compared wrt. first component (the atomic type), not the duplicated sort;
* extra sorts are grounded towards fixed 'a, potentially with different sorts (the original version with Name.names could cause name clashes with other present variables, too, but this should not be a problem);
* deriv_rule_unconditional ensures that proof terms are always maintained independently of the "proofs" flag -- this improves robustness and preserves basic PThm proofs required for extraction attributes, e.g. in theory HOL/Extraction;

simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;

renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);

do not open ML structures;

renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;

modernized structure Term_Ord;

normalized uncurry take/drop

--HG--
extra : rebase_source : 647c8b5a6641f0eef6d4d81646474d16388f9fb9

curried take/drop

--HG--
extra : rebase_source : 6e6b508d936640bef00f0ad0c4fb089ad5253ef0

generalized procs for rewrite_proof: allow skeleton;
fulfill_norm_proof: always normalize result here, no re-normalization after filling;

adapted Theory_Data;
tuned;

revert fulfill_proof_future tuning (actually a bit slower due to granularity issues?);

fulfill_proof_future: tuned important special case of singleton promise;

standardized filter/filter_out;

curried union as canonical list operation

dropped redundant gen_ prefix

replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;

eliminated redundant parameters;

explicit indication of Unsynchronized.ref;

fold_body_thms: pass pthm identifier;
fold_body_thms: dismiss path-etic attempt to check for cycles (cf. e24acd21e60e) -- could be masked by "seen";
fulfill_proof/thm_proof: check for thm cycles at the substitution point;

fold_body_thms/join_bodies: explicitly check for cyclic theorem references;

get_name: cover only PThm, not PAxm;

prefer simultaneous join -- for improved scheduling;

tuned;

added join_bodies;

tuned prf_subst: use structure Same;

tuned/modernized Envir.subst_XXX;

tuned/modernized Envir operations;

tuned incr_indexes;

tuned map_proof_terms_option;
eliminated apsome, apsome';
tuned;

use structure Same;
do not open Envir;

renamed structure TermSubst to Term_Subst;

renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;

added pro-forma proof constructor Inclass;

removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
added approximate_proof_body -- replaces former make_proof_body;
added all_oracles_of;
oracle_proof: explicit oracle result;
fulfill_proof/thm_proof: require proper proof_body futures, to maintain full account of oracles and thms (repairs a serious problem of the old version);

status_of: simultaneous list;

display derivation status of thms;

Merge.

eliminated NJ's List.nth;

thm_proof: recovered single-threaded version;

thm_proof: replaced lazy by composed futures;

proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;

moved old add_term_vars, add_term_frees etc. to structure OldTerm;

freeze_thaw: canonical Term.add_XXX operations;
varify: regular name context;

renamed type Lazy.T to lazy;

tuned;

eliminated finish_proof, keep pre/post normalization of results separate;

fulfill_proof/thm_proof: commuted lazyness;

finish_proof: undefined promises may occur here;

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;

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

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.

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;

added conditional add_oracles, keep oracles_of_proof private;
added fulfill;
removed unused is_named;
tuned some table operations;

added Promise constructor, which is similar to Oracle but may be replaced later;
added promise_proof;
export min_proof, mk_min_proof;
moved infer_derivs to thm.ML as derive_rule0/1/2;
tuned oracles_of_proof;
added is_named;

Logic.all/mk_equals/mk_implies;

rep_cterm/rep_thm: no longer dereference theory_ref;
removed obsolete compression;

eliminated theory ProtoPure;

Type.lookup now curried

Added function rew_proof (for pre-normalizing proofs).

Adapted Proofterm.bicompose_proof to Larry's changes in
Logic.assum_pairs from 2005-01-24 (revision 1.44).

simplified/unified list fold;

simplified DataFun interfaces;

canonical merge operations

thm/prf: separate official name vs. additional tags;

*** empty log message ***

renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);

moved term subst functions to TermSubst;

replaced maxidx_of_proof by maxidx_proof;

tuned;

fold_proof_terms: canonical arguments;
removed obsolete add_prf_names, add_prf_tfree_names, add_prf_tvar_ixns;

replaced Term.variant(list) by Name.variant(_list);

added map_proof_terms_option;
tuned generalize, instantiate;

added generalize rule;

tuned;

tuned basic list operators (flat, maps, map_filter);

Added alternative version of thms_of_proof that does not recursively
descend into proofs of (named) theorems.

remove (op =);
tuned;

infer_derivs: avoid allocating empty MinProof;

tuned;

subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate

bicompose_proof: no_flatten;

Improved norm_proof to handle proofs containing term (type) variables
with same name but different types (sorts): Offending term (type)
variables are replaced by dummy (T)Frees before applying the
substitution.

Logic.lift_all;

minor tweaks for Poplog/ML;

shrink: compress terms and types;
prefer member/insert over polymorphic mem/ins;

TableFun/Symtab: curried lookup and update;

introduced new-style AList operations

introduces some modern-style AList operations

curried_lookup/update;

refer to theory instead of low-level tsig;

- Tuned handling of oracles
- Put arguments of axms_of_proof and thms_of_proof into "canonical order"

replaced atless by term_ord;

adapted Type.typ_match;
tuned;

tuned instantiate interface;
Logic.incr_tvar;

(intermediate commit)

renamed init to init_data;

accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;

- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.

op vor infix-Konstruktoren im datatype binding zum besseren Parsen

Removed practically all references to Library.foldr.

Move towards standard functions.

Deleted Library.option type.

- Expressed infer_derivs' in terms of infer_deriv
- Eta-expanded function instantiate to delay evaluation (avoids inefficiencies
when proof terms are switched off)

Merged in license change from Isabelle2004

removed obsolete sort 'logic';

adapted tsig interface;

size_of_proof no longer includes size_of_term

Added size_of_proof.

Removed Logic.strip_flexpairs.

take/drop -> splitAt

thms/axms_of_proof: proper handling of MinProof;

Added skeletons to speed up rewriting on proof terms.

fixed get_name_tags in order to work with hyps;

New function change_type for changing type assignments of theorems,
axioms and oracles.

made MLWorks happy;

Added function could_unify to speed up rewriting of proof terms.

New function maxidx_of_proof.

type_env;

theory data: removed obsolete finish method;

fixed SML/NJ error (!?);

use merge_lists, merge_alists;

Extended match_proof to handle abstractions.

- Fixed bug in shrink
- Restored old behaviour of thm_proof
- Eliminated reference from theory data

theory data: finish method;

Fixed bug in function add_npvars.

Tuned function thm_proof.

Tuned several functions to improve sharing of unchanged subproofs.

eta-expansion required for SML/NJ

- Exchanged % and %%.
- Fixed bug in shrink.

renamed `keep_derivs' to `proofs', and made an integer;

fixed header;

New implementation of LF style proof terms.