add real_le_linear to list of legacy theorem names

make SML/NJ happy

removed unused conversions;

tuned header; tuned white space;

moved normarith.ML where it is actually used; less inaccurate dependencies;

incorporated further conversions and conversionals, after some minor tuning;

eliminated redundant runtime checks;

normalize atyp names after unconstrainT, which may rename atyps arbitrarily;

more precise dependencies for HOL-Word-SMT_Examples;

merged

merge

added Sledgehammer documentation to TOC

added some Sledgehammer news

document Nitpick changes

merge

added Sledgehammer manual; some material was recovered from the Isar material, the rest is new

renamed Sledgehammer options

renamed options

remove support for crashing beta solver HaifaSat

renamed two Sledgehammer options

merged

added listsum lemmas

Revert mixin patch due to inacceptable performance drop.

add "no_atp"s to Nitpick lemmas

query _HOME environment variables at run-time, not at build-time

move Refute dependency from Plain to Main

move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong

recognize new Kodkod error message syntax

improve precision of set constructs in Nitpick

produce more potential counterexamples for subset operator (cf. quantifiers)

improved Sledgehammer proofs

pass "full_type" argument to proof reconstruction

made Sledgehammer's full-typed proof reconstruction work for the first time; previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code

delect installed ATPs dynamically, _not_ at image built time

Fix syntax; apparently constant apply was introduced in an earlier changeset.

Merged.

Add mixin to base morphism, required by class package; cf ab324ffd6f3d.

Remove improper use of mixin in class package.

Multiset: renamed, added and tuned lemmas; Permutation: replaced local "remove" by List.remove1

use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document

more precise dependencies

updated SMT certificates

layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable

integrated SMT into the HOL image

replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite

use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)

split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)

added tracing of reconstruction data

added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms

deleted SMT translation files (to be replaced by a simplified version)

move the addition of extra facts into a separate module

normalize numerals: also rewrite Numeral0 into 0

added missing rewrite rules for natural min and max

rewrite bool case expressions as if expression

simplified normalize_rule and moved it further down in the code

merged addition of rules into one function

added simplification for distinctness of small lists

moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)

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;

the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;

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;

conditional structure SingleAssignment;

merged

merged

tuned proofs and fact and class names

tuned fact collection names and some proofs

grouped local statements

tuned test problems

merged

merged

simplified proof

modernized specifications;

updated/unified some legacy warnings;

tuned;

do not emit legacy_feature warnings here -- users have no chance to disable them;

removed obsolete CVS Ids;

removed some obsolete admin stuff;

check NEWS;

removed obsolete CVS Ids;

updated some version numbers;

minor tuning;

reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only; (Spelling note: "supersede" is indeed more common in Isabelle sources, although "supercede" is also correct according to major dictionaries.)

merged

merged

modernized specifications; tuned reification

merged

added lemmas concerning last, butlast, insort

Remove RANGE_WARN

clarified NEWS entry

merged

added NEWS entry

Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'

Add rules directly to the corresponding class locales instead.

Removed usage of normalizating locales.

speed up some proofs, fixing linarith_split_limit warnings

fix some linarith_split_limit warnings

include iszero_simps in semiring_norm just once (they are already included in rel_simps)

fix duplicate simp rule warning

no more RealPow.thy (remaining lemmas moved to RealDef.thy)

merged

simplify code for emptiness check

removed lemma real_sq_order; use power2_le_imp_le instead

merged

merged

represent de-Bruin indices simply by position in list

tuned reification functions

tuned code; toward a tightended interface with generated code

fix spelling of 'superseded'

NEWS: removed theory PReal

collected NEWS updates for HOLCF

merged

move floor lemmas from RealPow.thy to RComplete.thy

add lemma tendsto_Complex

move some theorems from RealPow.thy to Transcendental.thy

add lemma power2_eq_1_iff; generalize some other lemmas

minimize imports

move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff

clarified Pretty.font_metrics;

format as topmost list of "divs", not just adjacent "spans" -- for proper line breaking;

tuned;

more precise pretty printing based on actual font metrics; removed obsolete relative margin;

predefined spaces;

merged

support Isabelle plugin properties with defaults; font size relative to view.textsize of jEdit; margin relative to component width and approximative font metrics;

merged

tuned proof so that no simplifier warning is printed

renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution

merged

tuned

theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct

tuned; dropped strange myassoc2

stylized COOPER exception

simplified oracle

shorten names

updated references to ML files

only one module fpr presburger method

moved int induction lemma to theory Int as int_bidirectional_induct

tuned theory text; dropped unused lemma

one structure is better than three

less complex organization of cooper source code

dropped unused bindings; avoid open (documents dependency on generated code more explicitly)

add real_mult_commute to legacy theorem names

new construction of real numbers using Cauchy sequences

add more credits to ex/Dedekind_Real.thy

put construction of reals using Dedekind cuts in HOL/ex

disable two stage save by default, to avoid change of file permissions (notably the dreaded executable bit on Cygwin);

simple dialogs: ensure Swing thread;

font size re-adjustment according to Lobo internals;

Scala for Netbeans 6.8v1.1.0rc2;

more convenient get_font;

renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;

more convenient look-and-feel setup;

more convenient get_font;

explicit getLines(n) ensures platform-independence -- our files follow the POSIX standard, not DOS;

updated to jedit 4.3.2;

ignore spurious TIMEOUT messages, maybe caused by change of actor semantics in scala-2.8;

adapted to scala-2.8.0.RC2;

merged

real_mult_commute -> mult_commute

avoid using real-specific versions of generic lemmas

avoid using real-specific versions of generic lemmas

remove a couple of redundant lemmas; simplify some proofs

merged

add lemmas one_less_inverse and one_le_inverse

do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings

added lemmas rel_comp_UNION_distrib(2)

made SML/NJ happy;

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;

added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);

tuned;

removed unused "option" variants of "same" operations;

more basic replacement of newlines;

static Symbol.spaces;

proper use of var stopped;

removed junk;

tuned headers;

tuned;

merged

merged

moved normalization proof tool infrastructure to canonical algebraic classes

added lemmas

merged

renamed Normalizer to the more specific Semiring_Normalizer

delete Groebner_Basis directory -- only one file left

split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces

merged