removed some non-essential rules

removed some lemma duplicates

--HG--
extra : rebase_source : e56adb958684d57563b0ec467d4b13f1b726b4e0

more symbols;

more symbols;

speed up proofs slightly

avoid effectively subsumed rules;
simplified fact reference

eliminated irregular aliasses

clarified theorem names

more standardized theorem names for facts involving the div and mod identity

use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable

invoke argo as part of the tried automatic proof methods

dropped various legacy fact bindings

prefer symbols for "abs";

isabelle update_cartouches -c -t;

tuned signature;

isabelle update_cartouches;

more accurate keywords;

modernized header uniformly as section;

modernized setup;

eliminated redundancies;
more simp rules

--HG--
extra : rebase_source : d2f3410108e72d87e8aafe6b8721e88136c940cf

further downshift of theory Parity in the hierarchy

--HG--
extra : rebase_source : e7215b85854d21232ca65e2ca813246deda9624b

prefer ac_simps collections over separate name bindings for add and mult

reduced name variants for assoc and commute on plus and mult

added 'satx' proof method to Try0

moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
tuned presburger

--HG--
extra : rebase_source : 30fe190a27dae1b09024f4fdd70ee005a33e99ba

Renamed {left,right}_distrib to distrib_{right,left}.

prefer ML_file over old uses;

more standard method setup;

modernized obsolete old-style theory name with proper new-style underscore

--HG--
rename : src/HOL/SetInterval.thy => src/HOL/Set_Interval.thy

remove redundant lemmas

remove redundant lemmas

merged fork with new numeral representation (see NEWS)

avoid inconsistent sort constraints;

new fastforce replacing fastsimp - less confusing name

avoid using legacy theorem names

shorten names

updated references to ML files

only one module fpr presburger method

tuned theory text; dropped unused lemma

one structure is better than three

less complex organization of cooper source code

--HG--
rename : src/HOL/Tools/Qelim/generated_cooper.ML => src/HOL/Tools/Qelim/cooper_procedure.ML

moved lemma zdvd_period to theory Int

get rid of many duplicate simp rule warnings

renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields

--HG--
rename : src/HOL/Ring_and_Field.thy => src/HOL/Fields.thy
rename : src/HOL/OrderedGroup.thy => src/HOL/Groups.thy
rename : src/HOL/Ring_and_Field.thy => src/HOL/Rings.thy

moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly

cleanedup theorems all_nat ex_nat

corrected and unified thm names

moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac

moved import of module qelim to theory Presburger

simplified method setup;

unified type Proof.method and pervasive METHOD combinators;

Merge.

Removed redundant lemmas

removed subsumed lemmas

dropped Id

Replaced group_ and ring_simps by algebra_simps;
removed compare_rls - use algebra_simps now

enable eq_bin_simps for simplifying equalities on numerals

clarified dependencies between arith tools

simplified oracle interface;

Tuned and simplified proofs

moved op dvd to theory Ring_and_Field; generalized a couple of lemmas

separate class dvd for divisibility predicate

moved some code lemmas for Numerals to other theories

loads Tools/Qelim/qelim.ML

New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1

added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps

joined theories IntDef, Numeral, IntArith to theory Int

continued localization

class div inherits from class times

tuned;

proper context for cooper_tac within arith;

arith method setup: proper context;

code lemma for of_int

moved lemma zdvd_period here

tuned and renamed group_eq_simps and ring_eq_simps

section headings

moved Presburger setup back to Presburger.thy;

renamed NatSimprocs.thy to Arith_Tools.thy;
incorporated HOL/Presburger.thy into NatSimprocs.thy;

adapted tool setup;

remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int

section headings

moved lemma all_not_ex to HOL.thy ; tuned proofs

Added some lemmas to default presburger simpset; tuned proofs

tuned proofs: avoid implicit prems;

removed constant int :: nat => int;
int is now an abbreviation for of_nat :: nat => int

Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts

A new and cleaned up Theory for QE. for Presburger arithmetic

tuned comments;

moved Integ files to canonical place;

fixed title;

moved Integ files to canonical place;

cleaned up code generator setup for int

Isar definitions are now added explicitly to code theorem table

tuned code theorems for ord on integers

A few theorems on integer divisibily.

dropped eq const

moved HOL code generator setup to Code_Generator

improved numeral handling for nbe

got rid of Numeral.bin type

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

tuned;

presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy

renamed rules to iprover

The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
comm_ring : a reflected Method for proving equalities in a commutative ring

improved oracle setup;

migrated theory headers to new format

import -> imports

New theory header syntax.

new treatment of binary numerals

Merged in license change from Isabelle2004

Oracle corrected

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

changes made due to new Ring_and_Field theory

tuned document;

new material from Avigad

generic of_nat and of_int functions, and generalization of iszero
and neg

Added lemmas to Ring_and_Field with slightly modified simplification rules

Deleted some little-used integer theorems, replacing them by the generic ones
in Ring_and_Field

Consolidated integer powers

Simplification of the development of Integers

cleaned up

New decision procedure for Presburger arithmetic.