more robust: proper transfer if Context.eq_thy_id;

more thorough strip_shyps for proof boxes (but types are usually stripped and reconstructed later);

tuned signature;

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

proper sort constraints for strip_shyps, for sort relations used in minimization;

tuned;

proper sort constraints for strip_shyps, which implicitly performs type instantiation;
include solve_constraints in strip_shyps to avoid later conflicts with Thm.transfer;

more structural integrity;

clarified modules;

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;

expose derivations more thoroughly, notably for locale/class reasoning;

more robust;

clarified modules;

clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;

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

tuned signature;

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;

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

tuned -- more direct ML expressions;

clarified modules;

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

misc tuning and clarification;

tuned -- allow slightly more expensive atomic proofs;

clarified signature: prefer total operations;

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

tuned;

unused (see 095dadc62bb5);

tuned;

clarified signature;

discontinued peek_status: unused and not clearly defined;

added ML antiquotation @{oracle_name};

more robust, notably for open_proof of unnamed derivation;

added command 'thm_oracles';

unused;

clarified signature;

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

clarified derivation_name vs. raw_derivation_name;

more robust -- notably for metis, which tends to accumulate tpairs;

record sort constraints unconditionally: minimal performance implications;

formal position for PThm nodes;

more robust and convenient treatment of implicit context;

explicit check of left-over constraints from different theory, e.g. due to lack of Thm.trim_context;

backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker;

more robust and convenient treatment of implicit context;

clarified modules: more direct data implementation;

more efficient data structure;

guard constraints by record_proofs=1, until performance implications have become more clear;

more complete completions according to Sorts.insert_complete_ars (cf. 13199740ced6), e.g. relevant for theories HOL-ex.Word_Type, HOL-Matrix_LP.SparseMatrix;

tuned;

tuned;

maintain sort constraints from type instantiations, with pro-forma derivation to collect oracles/thms;
tuned;

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

tuned;

clarified modules: inference kernel maintains sort algebra within the logic;

clarified module structure;

simplified module structure: back to plain datatype (see 95f4f08f950f and 70019ab5e57f);

clarified modules;

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

more structural integrity;

clarified transfer_morphism: implicit join_certificate, e.g. relevant for complex cascades of morphisms such as class locale interpretation;

tuned signature;

more ctyp operations;

prefer exception TYPE, e.g. when used within conversion;

tuned signature -- more ctyp operations;

more direct implementation of distinct_subgoals_tac -- potentially more efficient;

proper maxidx: if x does not occur in A, its maxidx could get lost;

tuned;

eliminated ASCII syntax from Pure bootstrap;
tuned comments;

more operations for ctyp, cterm;

tuned signature;

repaired whitespace accident from 2505cabfc515

proper namespace for evaluators

--HG--
extra : rebase_source : cbf47061c33ac1e0a221ab6513662ecd3e78c71d

consolidate proofs more simultaneously;

tuned signature;

proper background certificate from make_context, which can be a super-theory of the direct join (amending d07464875dd4);

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;

back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);

more careful derivation_closed / close_derivation;

tuned;

tuned whitespace;

tuned;

clarified exceptions;
tuned signature;

clarified exceptions;
more careful treatment of missing context;

trim context for persistent storage;

clarified exceptions;

clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);

more abstract theory certificate, which is not necessarily the full theory;

tuned signature;

tuned signature;

produce certified vars without access to theory_of_thm, and without context;

produce certified vars without access to theory_of_thm, and without context;

added Thm.chyps_of;
eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);

prefer theory_id operations;
tuned signature;

obsolete;

more direct access to atomic cterms;

simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);

tuned signature;

more explicit context;

explicitly checked alpha conversion -- actual renaming happens outside kernel;

more uniform "verbose" option to print name space;

tuned signature;

local fixes may depend on goal params;

Thm.cterm_of and Thm.ctyp_of operate on local context;

tuned signature;

removed unused;
tuned comments;

clarified signature;

tuned signature -- prefer qualified names;

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

optional proof context for unify operations, for the sake of proper local options;

proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago);

eliminated aliases;

more qualified names;

tuned signature;

abstract type Name_Space.table;
clarified pretty_locale_deps: sort strings;
clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;

tuned;

type theory is purely value-oriented;

turned pattern unify flag into configuration option (global only);

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;

tuned signature -- more explicit flags for low-level Thm.bicompose;

unify types of schematic variables in non-lifted case (i.e. "compose variants") -- allow schematic polymorphism, without revisiting HO-unification;

tuned signature;

updated comment to 46b90bbc370d;

print formal entities with markup;

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;

proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);

prefer canonical fold_rev;

maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global);
prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output);
simplified signatures;

renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;

tuned signature;

removed obscure/outdated material;

renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;

renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;

discontinued unused Thm.compress (again);

tuned signature;

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;

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;

more systematic handling of parallel exceptions;
distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;

rename_bvs now avoids introducing name clashes between schematic variables

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

tuned signature -- corresponding to Scala version;

more robust exception pattern General.Subscript;

added Theory.nodes_of convenience;

report Name_Space.declare/define, relatively to context;
added "global" variants of context-dependent declarations;

modernized structure Proof_Context;

Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;

thm_proof: visible fulfill_body only, without joining nested thms -- retain proof irrelevance, which is important for parallel performance;

tuned comments;

type attribute is derived concept outside the kernel;

recovered some odd two-dimensional layout;

modernized structure Ord_List;

structure Thm: less pervasive names;

eliminated ML structure alias;

always unconstrain thm proofs;

dropped legacy_unconstrainT

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;

reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;

Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;

just one version of Thm.unconstrainT, which affects all variables;
temporary workaround for Nbe.lift_triv_classes_conv;

renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;

tuned signature;

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;

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

renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;

minor tuning of Thm.strip_shyps -- no longer pervasive;

simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;

renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
less pervasive names;

added Term.fold_atyps_sorts convenience;

Logic.mk_of_sort convenience;

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

explicitly mark some legacy freeze operations;

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

tuned;

adapted Theory_Data;
tuned;

make SML/NJ happy;

maintain explicit name space kind;
export Name_Space.the_entry;
tuned messages;

renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;

curried inter as canonical list operation (beware of argument order)

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

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;

tuned internal source structure;

replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;

lambda/cabs/all: named variants;

simultaneous join_proofs;
removed obsolete promises_of;

prefer simultaneous join -- for improved scheduling;

support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies);
export promises_of;
removed obsolete pending_groups;
tuned;

tuned/modernized Envir.subst_XXX;

tuned/modernized Envir operations;

tuned incr_indexes;

renamed structure TermSubst to Term_Subst;

clarified strip_shyps: proper type witnesses for present sorts;
moved fold_terms to thm.ML;

structure Thm: less pervasive names;

clarified Thm.of_class/of_sort/class_triv;

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

strip_shyps: remove top sort, which is logically insignificant;

added pro-forma proof constructor Inclass;

fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete);
more explicit oracle_proof;

status_of: need to include local promises as well!

display derivation status of thms;

eq_assumption: slightly more efficient by checking (open) result of Logic.assum_problems directly;
tuned;

substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);

renamed NameSpace.bind to NameSpace.define;

moved Thm.def_name(_optional) to more_thm.ML;
moved old-style Thm.get_def to Drule.get_def;

Thm.add_oracle interface: replaced old bstring by binding;

thm_proof: replaced lazy by composed futures;

future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);

added pending_groups -- accumulates task groups of local derivations only;

avoid polymorphic equality;

use regular Term.add_XXX etc.;

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

renamed force_proof to join_proof;

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;

dropped NameSpace.declare_base

future proofs: pass actual futures to facilitate composite computations;
removed join_futures -- superceded by higher-level PureThy.force_proofs;

cleaned up binding module and related code

future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);

fulfill_proof/thm_proof: commuted lazyness;
join_futures: Exn.release_all is back again (still required for implicit join of Toplevel.excursion);

added force_proofs;
join_futures: no errors here;

tuned promise/fullfill;

put_name/thm_proof: promises are filled with fulfilled proofs;
tuned;

clarified Thm.proof_body_of vs. Thm.proof_of;

refined notion of derivation, consiting of promises and proof_body;
removed oracle_of (would require detailed check wrt. promises);
proof_of returns proof_body;

renamed get_axiom_i to axiom, removed obsolete get_axiom;
reduced pervasive names;

join results in isolation;

added weaken_sorts;
strip_shyps: minimal list of minimized extra sorts;
tuned;

renamed promise to future, tuned related interfaces;

more precise join_futures, improved termination;

export explicit joint_futures, removed Theory.at_end hook;
renamed Future.fork_irrelevant to Future.fork_background;

join earlier promises first;

promise_result: enforce strictly sequential dependencies, via serial numbers;

Future.release_results;

promise: include check into future body, i.e. joined results are always valid;
pending future derivations: shared ref within whole theory body, i.e. end-of-theory joins *all* derivations ever forked from a version of the theory;
simplified rep_deriv;

simplified promise;
fulfill is internal only;
more robust join_futures;

abtract types: plain datatype with opaque signature matching;
promise: join pending futures at end of theory;

explicit type OrdList.T;

added dest_deriv, removed external type deriv;
misc tuning of internal deriv;
more substantial promise/fulfill;
promise_ord: reverse order on serial numbers;
removed unused is_named;
get_name: unfinished proof term;

type thm: fully internal derivation, no longer exported;
incorporate former deriv.ML as internal abstract type;
added rudimentary promise interface;
tuned;
added is_named (does not require finished derivation);

simplified oracle interface;

added deriv.ML: Abstract derivations based on raw proof terms.

type Properties.T;

Logic.all/mk_equals/mk_implies;
Term.all;

moved global pretty/string_of functions from Sign to Syntax;

eq_assumption now uses aeconv instead of aconv.

Theory.eq_thy;

simplified handling of sorts, removed unnecessary universal witness;
Envir.insert_sorts;

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

eliminated theory ProtoPure;

Removed Logic.auto_rename.

replaced literal 'a by Name.aT;

compress: proper check_thy;

replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
thread-safeness: when creating certified items, perform Theory.check_thy *last*;

Added function norm_proof for normalizing the proof term
corresponding to a theorem.

thm tag: Markup.property list;

added type conv;
merge_thys: removed dead exception handlers;
tuned;

added eta_long_conversion;

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

simplified/unified list fold;

added dest_fun/fun2/arg1;
removed dest_binop;
renamed cterm_(fo_)match to (fo_)match;
renamed cterm_incr_indexes to incr_indexes_cterm;

removed obsolete read_ctyp, read_def_cterm;
moved read_def_cterms, read_cterm to more_thm.ML;
avoid rep_theory;

rep_thm/cterm/ctyp: removed obsolete sign field;

improved exception CTERM;
added instantiate_cterm;
removed obsolete sign_of_thm;

avoid clash with Alice keywords;

moved some non-kernel material to more_thm.ML;

old-fashioned abstype ctyp/cterm/thm prevents accidental equality tests;

Term.lambda: abstract over arbitrary closed terms;

tuned error messages;

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

simplified Logic.count_prems;

moved theorem kinds from PureThy to Thm;

removed obsolete first_duplicate;

fixed type signature of Type.varify

abandoned findrep

added def_name_optional;

cterm_match: avoid recalculation of maxidx;

added dest_binop;

added dest_arg, i.e. a tuned version of #2 o dest_comb;

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

instantiate: omit has_duplicates check, which is irrelevant for soundness;

ctyp: maintain maxidx;
cterm_match: tight maxidx for substitution;
instantiate: determine maxidx from insts -- major performance improvement;
moved term subst functions to TermSubst;
tuned;

abandoned equal_list in favor for eq_list

tuned;

normalized Proof.context/method type aliases;

adjust_maxidx: pass explicit lower bound;
tuned interfaces;

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

tuned exception handling;

varifyT: no longer pervasive;

added generalize rule;
added maxidx_thm;

added hyps_of;
tuned;

tuned Seq/Envir/Unify interfaces;

class_triv: Sign.certify_class;

added unconstrainT;

curried Seq.cons;

added maxidx_of;

avoid polymorphic equality;

Shortened the exception messages from assume.

tuned;

removed obsolete sign_of_cterm;
adapted Sign.certify_term;

union_tpairs: Library.merge;
Envir.(beta_)eta_contract;
tuned;

simplified type attribute;
added rule/declaration_attribute (from drule.ML);
added theory/proof_attributes;
removed apply(s)_attributes;

turned bicompose_no_flatten into compose_no_flatten, without elimination;

added bicompose_no_flatten, which refrains from
changing the shape of the new subgoals;

re-arranged tuples (theory * 'a) to ('a * theory) in Pure

tuned Pattern.match/unify;

renamed Thm.cgoal_of to Thm.cprem_of;

Thm.varifyT': natural argument order;

added cgoal_of;
simplified lift_rule: take goal cterm instead of goal state thm, use Logic.lift_abs/all;

tuned comment;

abstract_rule: tuned exception msgs;

TableFun/Symtab: curried lookup and update;

added simple_fact;
generalized no_attributes;

curried_lookup/update;

refer to theory instead of low-level tsig;

use AList operations;

Compress.term;

added weaken, adjust_maxidx_thm;

tuned instantiate (avoid subst_atomic, subst_atomic_types);
Logic.incr_tvar;

invoke_oracle: do not keep theory value, but theory_ref;

added full_prop_of: includes tpairs;

tuned maxidx;

dest_ctyp: raise exception for non-constructor;
dest_comb: replaced expensive fastype_of by Term.argument_type;
dest_abs: replaced expensive variant_abs by Term.dest_abs;
hyps: fast_term_ord;

ctyp: added 'sorts' field;
may_insert_typ/term/env_sorts: observe Sign.all_sorts_nonempty;
may_insert_env_sorts: insert sorts of type subst only;
instantiate: insert sorts of insts;
tuned;

more efficient treatment of shyps and hyps (use ordered lists);
added 'sorts' field to cterm;
removed obsolete fix_shyps;
moved implies_intr_hyps to drule.ML;

accomodate identification of type Sign.sg and theory;

axioms: NameSpace.table;

Type.freeze;

added eq_thms;

tuned terms_of_tpairs;

- 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.

added get_axiom_i, invoke_oracle_i;

Removed practically all references to Library.foldr.

Move towards standard functions.

Deleted Library.option type.

thin_tac now works on P==>Q

Changed function cabs to also allow abstraction over Vars.

- optimized nodup_vars check in capply
- new function dest_ctyp

improved output; refer to Pretty.pp;

adapted names of some sort ops;

Changed handling of flex-flex constraints: now stored in separate
tpairs field of theorem record.

added failure trace information to pattern unification

take/drop -> splitAt

added proof_of;

moved match_bvs, match_bvars, renAbs to term.ML;

fixed get_name_tags in order to work with hyps;

added prop_of: thm -> term (at last!);

varifyT' returns newly introduces variables;

major_prem_of: Logic.strip_assums_concl;

Exchanged % and %%.

Fixed proof term bug in permute_prems.

Replaced old derivations by proof terms.

Thm: dest_comb, dest_abs, capply, cabs no longer global;

Envir.beta_norm;

- Moved rewriting functions to meta_simplifier.ML
- dest_abs now also takes an optional variable name as an argument
- beta_conversion takes additional flag as an argument. Fully reduces
the term if set to true

Some tuning:
- tuned fix_shyps in instantiate, implies_intr, implies_elim, reflexive,
transitive, beta_conversion, abstract_rule
- combination: chktypes derives types of f and t from type of == instead
of using fastype_of

New primitives:
- eta_conversion
- incr_indexes: increment indexes in theorems
- cterm_incr_indexes: increment indexes in cterms
- cterm_match, cterm_first_order_match
- rename_boundvars

back to 1.167, due to Emacs/CVS casualty!!;

*** empty log message ***

Added meaningful output to cong-error msg.

*** empty log message ***

Fixed completeness bug in simplifier: congruence rules could preclude
rewrites of the partially applied constant.

derivations: maintain oracle flag;

added sign_of_cterm;

fixed Thm.eq_thm: use Sign.joinable;

dest_mss: sort procs wrt. names;

tuned msg;

read_def_cterms: use Sign.read_def_terms;

Envir now uses Vartab instead of association lists.

added major_prem_of;

tuned;

capply, cabs: Sign.nodup_vars;

Thm.instantiate no longer normalizes, but Drule.instantiate does

SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
nested parameters such as !!y.

Goal "!!x. x = a ==> (!!y. y ~= a ==> False)";
by (rotate_tac 1 1);
be notE 1;
ba 1;
qed "foo";

val FalseI = standard (True_not_False RS (standard (refl RS foo)));

debug_simp;

removed implies_intr_shyps;
removed force_strip_shyps (at last!);
strip_shyps: proper witness_sorts;
fix_shyps: tuned for all_sorts_nonempty;

added no_prems;

removed obsolete comment;

Now rewrite rules with flexible heads are allowed.

Corrected two busg in the simplifier.

(*no fix_shyps*);

new primitive rule permute_prems to underlie defer_tac and rotate_prems

tuned add_term_varnames;

improved error msgs of instantiate;

added clear_mss;

varifyT': observe additional 'fixed' tfrees;

Eta contraction is now performed all the time during rewriting.

qualify Theory.sign_of etc.;

added def_name;
class_triv: Sign.sg;

signature BASIC_THM;
theorem / axiom deriv: added tags;
get/put_name_tags;
type attribute;

Further improvement of the simplifier.

Tuned simplifier not to re-normalized already normalized terms.

improved error messages

assume: adjust_maxidx;

The warning "Rewrite rule from different theory" is ALWAYS printed, even if
tracing is off.

Object.T;

tuned get_ax (uses ancestry);
added get_def: theory -> xstring -> thm;

Tried to speed up the rewriter by eta-contracting all patterns beforehand and
by classifying each pattern as to whether it allows first-order matching.

tuned trace msgs;

Made mutual simplification of prems a special case.

Asm_full_simp_tac now reorients asm c = t to t = c.

New simplifier flag for mutual simplification.

Removed superfluous `op'

Reorganized simplifier. May now reorient rules.
Moved loop tests from logic to thm.

Tried to reorganize rewriter a little. More to be done.

improved tracing of rewrite rule application;

Term.termless;

tuned msg;

removed read_cterms;

added crep_cterm;

Added read_def_cterms for simultaneous reading/typing of terms under
defaults.
Redefined read_def_cterm in in terms of read_def_cterms.
Deleted obsolete read_cterms.

Cleaned up def of read_insts, which is not much shorter but much clearere are
correcter now.

changed Sequence interface (now Seq, in seq.ML);

added transfer_sg;

tuned infer_types interface;

deriv: eliminated references to theory;

type object = exn (enhance readability);

logic: loops -> rewrite_rule_ok
added rewrite_rule_extra_vars

thm: Rewrite rules must not introduce new type vars on rhs.
This lead to an incompleteness, is now banned, and the code
has been simplified.

Modified trace output routines of simplifier.

tuned simp trace;

added name_of_thm;
improved name_thm: does not overwrite existing name;

eq_thm (from drule.ML);

tuned;

tuned;

sg_ref: automatic adjustment of thms of draft theories;

added transfer: theory -> thm -> thm;

The simplifier has been improved a little: equations s=t which used to be
rejected because of looping are now treated as (s=t) == True. The latter
translation must be done outside of Thm because it involves the object-logic
specific True. Therefore the simple loop test has been moved from Thm to
Logic.

fixed get_axiom, invoke_oracle;
improved Oracle deriv;

tuned read_cterms;

added prems argument to simplification procedures;

Now rename_params_rule merely issues warnings--and does nothing--if the
renaming cannot be performed. Previously it raised a fatal error.

improved simp tracing;

added dest_mss, merge_mss;
fixed matching of simproc lhss;

tuned warning;
improved comments;

freezeT now refers to Type.freeze_thaw

improved tmp comment;

rename_params_rule used to check if the new name clashed with a free name in
the whole goal state. Now checks only the subgoal concerned.

simprocs called with eta contracted subterm;

improved type check error messages;

Sorts.str_of_sort;

Avoid eta-contraction in the simplifier.
Instead the net needs to eta-contract the object.
Also added a special function loose_bvar1(i,t) in term.ML.

Introduction of rotate_rule

added del_congs

Made troublesome simplifier warning dependent on trace_simp.

Added warning msg when the simplifier cannot use a premise as a rewrite rule
because it contains (type) unknowns.

added termless parameter;
added simplification procedures;

fixed warning;

Replaced map...~~ by ListPair.map

Changed subst_bounds to subst_bound, to run faster

Removal of polymorphic equality via mem, subset, eq_set, etc

Changed some mem, ins and union calls to be monomorphic

tuned fix_shyps a little bit more;

Now uses Int.max instead of max
nodup_Vars now updates maxidx

Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%

added shyps comment;

Inserted check for rewrite rules which introduce extra Vars on the rhs.

Added type-checking to rule "combination". This corrects a fault
concerning soundness. See Jeremy Dawsons message of 27 Jun 1996 on
isabelle-users

Now del_simp catches the right exception!

moved dest_cimplies to drule.ML; added adjust_maxidx

*** empty log message ***

Plugged some more loopholes with nodup_Vars.

name_thm no longer takes a theory argument, as the
name no longer hides the previous derivation.

Deleted sign_of_thm as redundant.

Added some functions which allow redirection of Isabelle's output

Added some optimized versions of functions dealing with sets
(i.e. mem, ins, eq_set etc.) which do not use the polymorphic =
operator

Non-matching congruence rule in rewriter is simply ignored.
Used to cause error message.

name_thm: now keeps the previous deriviation!

Addition of oracles

Addition of proof objects

added cabs and crep_thm

removed mk_prop; added capply; simplified dest_abs

Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.

Added check for duplicate vars with distinct types/sorts (nodup_Vars)

added dest_comb, dest_abs and mk_prop for manipulating cterms

inserted tabs again

removed tabs

Commented the datatype declaration of thm.

Declared compress: thm -> thm to copy a thm and maximize sharing in it.

"ext_axms" now calls Term.compress_term so that stored axioms use sharing.

New function read_cterms is a combination of read_def_cterm and
read_cterm. It reads and simultaneously type-checks a list of strings.
cterm_of no longer catches exception TYPE; instead it must be caught later on
and a message printed using Sign.exn_type_msg. More informative messages can
be printed this way.

bicompose_aux: tuned fix_shyps;
simplifier: fixed handling of shyps;

considerably tuned shyps handling;

deactivated fix_shyps.

MAJOR changes:
added shyps component to type thm;
added rules strip_shyps, implies_intr_shyps;
fixed rules to handle shyps properly;

match_bvs no longer puts a name in the alist if it is null ("")

added add_trrules_i;
cleaned up signature THM;
improved some comments;

Fixed old bug in the simplifier. Term to be simplified now carries around its
maxidx. Needed for renaming rewrite or congruence rules. maxidx should be ~1
in most cases (ie no Vars), hence reasonable overhead.

Added comment to function "loops".

Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
the maxidx-filed of thms is computed correctly.

Simplification: used Logic.occs instead of mem add_term_frees

removed print_msg parameter of infer_types

Changed treatment of during type inference internally generated type
variables.

1. They are renamed to 'a, 'b, 'c etc away from a given set of used names.
2. They are either frozen (turned into TFrees) or left schematic (TVars)
depending on a parameter. In goals they are frozen, for instantiations they
are left schematic.

added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)

Improved test for looping rewrite rules.

Improved check for looping conditional rewrite rules.

improved axioms_of: returns thms as the manual says;

Pure/thm/norm_term_skip: new, for skipping normalization of the context

Pure/thm/bicompose_aux: now computes nlift (number of lifted assumptions in
new subgoals) and avoids normalizing the first nlift assumptions in the
case where the proof state is not affected.

Pure/thm/norm_term_skip: now normalizes types of parameters

Pure/thm/THM: aligned colons

Modified pattern.ML to perform proper matching of Higher-Order Patterns.
Modified thm.ML to preserve bound var names during rewriting.
Renamed eta_matches to matches.

Prepared the code for preservation of bound var names during rewriting. Still
requires a matching function for HO-patterns.

added print_msg;
added call of Type.infer_types to resolve ambiguities

Modified termord to take account of the Abs-Abs case.

read_def_cterm: minor changes;
merge_thm_sgs: improved error msg;

added inferT_axm;
removed extend_theory;
changed read_def_cterm: now uses Sign.infer_types;

fixed comment: "(| _ : _ |)" to "OFCLASS(_, _)"

rewritec now uses trace_thm for it's "rewrite rule from different theory"
message

Improved error msg "Proved wrong thm"

ordered rewriting applies to conditional rules as well now