tuned signature;

replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace

Integer.lcm normalizes the sign as in HOL/GCD.thy;
tuned;

tuned signature;

more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;

moved remaining display.ML to more_thm.ML;

simplified simproc programming interfaces;

trim context for persistent storage;

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

dropped dead code

tuned signature;

eliminated dead code (cf. 5e5c36b051af);

clarified context;

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

clarified signature;

tuned;

tuned signature -- prefer qualified names;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

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

eliminated aliases;

disabled counterexample output for now; confusing because often incorrect

tuned signature;

prefer explicitly qualified exceptions, which is particular important for robust handlers;

simplifier uses proper Proof.context instead of historic type simpset;

dropped some unused identifiers

prefer explicitly qualified exception List.Empty;

clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well;

proper config option linarith_trace;

tuned signature;

linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
control tracing of (potentially spurious) counterexamples by the configuration option "linarith_verbose" (to disable linarith traces entirely)

clarify warning message to avoid confusing beginners

tuned signature: Name.invent and Name.invent_names;

modernized structure Proof_Context;

added merge_options convenience;

replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;

Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;

slightly more abstract data handling in Fast_Lin_Arith;

dropped dead code

less pervasive names from structure Thm;

farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)

removed warning_count (known causes for warnings have been resolved)

removed e-mail address from error message

removed old CVS Ids;
tuned headers;

Use same order of neq-elimination as in proof search.

Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;

adapted Generic_Data, Proof_Data;
tuned;

standardized filter/filter_out;

eliminated some old folds;

curried union as canonical list operation

dropped redundant gen_ prefix

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

uniform use of Integer.add/mult/sum/prod;

replaced String.concat by implode;
replaced String.concatWith by space_implode;
replaced (Seq.flat o Seq.map) by Seq.maps;
replaced List.mapPartial by map_filter;
replaced List.concat by flat;
replaced (flat o map) by maps, which produces less garbage;

explicit indication of Unsynchronized.ref;

qualified Subgoal.FOCUS;

replaced old METAHYPS by FOCUS;

proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;

dropped find_index_eq

made SML/NJ happy

tuned

fast_lin_arith uses proper multiplication instead of unfolding to additions

mk_number replaces number_of

tuned error messages

Instead of giving up entirely, arith now ignores all inequalities when there are too many.

added warning_count for issued reconstruction failure messages (limit 10);
less nesting of let expressions;

renamed type decompT to decomp;
refute: proper context for trace_ex;
some attempts to improve readability;

Lookup and union operations on terms are now modulo eta conversion.

generic Syntax.pretty/string_of operations;

simplified type int (eliminated IntInf.int, integer);

simplified internal Config interface;

arith method setup: proper context;
turned fast_arith_split/neq_limit into configuration options;
tuned signatures;
misc cleanup;

renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;

avoid polymorphic equality;

tuned arithmetic modules

simplified type integer;

tuned integers

cosmetic

additional tracing information

fixed handling of meta-logic propositions

tuned

dropped nonsense comment

tuned

simplified DataFun interfaces;

rep_thm/cterm/ctyp: removed obsolete sign field;

removed obsolete sign_of/sign_of_thm;

dropped nth_update

lin_arith_prover: splitting reverted because of performance loss

type annotations fixed (IntInf.int, to make SML/NJ happy)

possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed

code reformatted

lin_arith_prover splits certain operators (e.g. min, max, abs)

linear arithmetic splits certain operators (e.g. min, max, abs)

tuned;

tuned;

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

Removed occurrences of makestring, which does not
exist in SML/NJ.

comment fixed

comment for conjI added

counter example: avoid vacuous trace;

setup: theory -> theory;

removed pointless trace msg.

introduced new map2, fold

cleaned up nth, nth_update, nth_map and nth_string functions

introduced functions from Pure/General/rat.ML

Simplifier.theory_context;

Simplifier.inherit_context instead of Simplifier.inherit_bounds;

Simplifier.inherit_bounds;

fixed syntax for sml/nj

Simplifier.inherit_bounds;

slight adaptions to library changes

introduced new-style AList operations

moved some rat functions to library.ML

takes & in premises apart now.

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

IntInf change

Use of IntInf.int instead of int in most numeric simprocs; avoids
integer overflow in SML/NJ

neqE applies even if the type is not one which partakes in linear arithmetic.
This lead to confusion. Now there are multiple type specific neqE.

handle Option instead of OPTION;

Move towards standard functions.

Deleted Library.option type.

made mult_mono_thms generic.

adapted type of simprocs;

avoid 'handle _' -- would cover Interrupt as well!!!

introduced fast_arith_neq_limit

Removed dangling exception handler

Finally fixed the counterexample finder. Can now deal with < on real.

Added an exception handler and error msg.

bug in counter example finder

for cancelling div + mod.

Added counter example generation.

Fixed two bugs

Big update. Allows case splitting on ~= now (trying both < and >).

use eq_thm_prop instead of slightly inadequate eq_thm;

updated debugging output

theory data: removed obsolete finish method;

gen_merge_lists';

use tracing function for trace output;

theory data: finish method;

rational arithemtic

towards rtional arithmetic

Now adjusted to mixed terms involving coercions.

avoid global references;

tracing flag for arith_tac

Commenst.

Restructured lin.arith.package.

Mod because of new solver interface.

Added comments.

Now distinguishes discrete from non-distrete types.

More arith refinements.

Simplified interface.

Split argument structure.

More arith simplifications.

Added simproc.

Small mods.

Version 1 of linear arithmetic for nat.

Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.