Syntax for the special cases Min(A`I) and Max (A`I)

ran isabelle update_op on all sources

more simplification rules

--HG--
extra : rebase_source : 2b7704ac9459d132ec9fea4769b865bdcad1548f

cleaned up and tuned

--HG--
extra : rebase_source : a1262817f08e7c73c1f578e8c3b21fcf9314f1fb

generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen

added lemmas and tuned proofs

--HG--
extra : rebase_source : 96f42feb3c60e71f2655c97d331ac68baf8b4a63

tuned imports

--HG--
extra : rebase_source : bc9797cb892085195c2d8662a7ca3896dd1e5011

more fundamental definition of div and mod on int

--HG--
extra : rebase_source : 95b72d036b88e199c61235ea5833a905f5632800

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

dropped superfluous preprocessing rule

moved some lemmas to appropriate places

--HG--
extra : rebase_source : d3d8537b1c25edc3e07620dda770ad1feb37ea72

A few new lemmas and needed adaptations

complete set of cases rules for integers known to be (non-)positive/negative;
legacy theorem branding

--HG--
extra : rebase_source : 536e611e197af7013710ab6a6a6f2463f5506066

setprod -> prod

setsum -> sum

more lemmas

--HG--
extra : rebase_source : f52072de0fdc0fac0b2505569668d385d1ffe93d

misc tuning and modernization;

"split add" -> "split"

tuned proofs -- avoid improper use of "this";

more canonical names

dropped various legacy fact bindings

generalized some lemmas;
moved some lemmas in more appropriate places;
deleted potentially dangerous simp rule

Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.

prefer symbols for "abs";

isabelle update_cartouches -c -t;

New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.

Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths

Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.

Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.

Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer

Rounding function, uniform limits, cotangent, binomial identities

added many small lemmas about setsum/setprod/powr/...

New lemmas

new lemmas and movement of lemmas into place

tuned proofs -- less legacy;

simplified simproc programming interfaces;

eliminated \<Colon>;

prefer symbols;

direct bootstrap of integer division from natural division

isabelle update_cartouches;

more theorems

tidying some messy proofs

Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy

The function frac. Various lemmas about limits, series, the exp function, etc.

tuned signature -- prefer qualified names;

eliminated technical fact alias

dropped redundancy

import general theorems from AFP/Markov_Models

modernized header uniformly as section;

some more facts on divisibility

generalized and consolidated some theorems concerning divisibility

moved lemmas out of Int.thy which have nothing to do with int

--HG--
extra : rebase_source : a6db16c774c1c078a2ed1a129509da61fa662a39

prefer ac_simps collections over separate name bindings for add and mult

reduced name variants for assoc and commute on plus and mult

avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.

--HG--
extra : rebase_source : 899541490c73fe6897445f97dc2a5a3c929cf153

simplify and fix theories thanks to 356a5efdb278

renamed 'fun_rel' to 'rel_fun'

remove simp rules made redundant by the replacement of neg_numeral with negated numerals

transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
* * *
compile
* * *
tuned imports to prevent merge issues in 'Main'

removed theory dependency of BNF_LFP on Datatype

moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain

--HG--
rename : src/HOL/FunDef.thy => src/HOL/Fun_Def.thy

prefer more canonical names for lemmas on min/max

eliminiated neg_numeral in favour of - (numeral _)

streamlined setup of linear arithmetic

more simplification rules on unary and binary minus

--HG--
extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1

restructed

--HG--
extra : rebase_source : 616c48d7ea31bebdcc552b6b49aa376ef8b2934a

killed most "no_atp", to make Sledgehammer more complete

use lifting_forget for deregistering numeric types as a quotient type

added lemma

migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

stronger reflexivity prover

split dense into inner_dense_order and no_top/no_bot

delete also predicates on relations when hiding an implementation of an abstract type

two target language numeral types: integer and natural, as replacement for code_numeral;
former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral;
refined stack of theories implementing int and/or nat by target language numerals;
reduced number of target language numeral types to exactly one

--HG--
extra : rebase_source : ffa0242ad108fe680ff144a716257c0784285d17

abandoned theory Plain

--HG--
extra : rebase_source : 6f5a395a55e8879386d1f79ab252c6fc2aca7dc5

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

prefer ML_file over old uses;

transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters

convert Int.thy to use lifting and transfer

--HG--
extra : rebase_source : 42849275130f48d9bee5b9e1dd82e9e9a0229b50

remove unnecessary simp rules involving Abs_Integ

--HG--
extra : rebase_source : c099a2f8080b9702edaa0d0f17fd4606880d59ef

removed Nat_Numeral.thy, moving all theorems elsewhere

load Tools/numeral.ML in Num.thy

set up numeral reorient simproc in Num.thy

move lemmas from Nat_Numeral to Int.thy and Num.thy

move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy

merged fork with new numeral representation (see NEWS)

adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets

semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat; attribute code_abbrev superseedes code_unfold_post

--HG--
extra : rebase_source : baeca2cb190a12d17b7906d2d74ff0cf73890c4e

prefer typedef without extra definition and alternative name;
tuned proofs;

eliminated obsolete "standard";

simplify some proofs

Int.thy: remove duplicate lemmas double_less_0_iff and odd_less_0, use {even,odd}_less_0_iff instead

removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)

inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);

removing old code generator setup for integers

Int.thy: discontinued some legacy theorems

introduce abbreviation 'int' earlier in Int.thy

move lemmas nat_le_iff and nat_mono into Int.thy

remove duplicate lemma nat_zero in favor of nat_0

modernized some simproc setup;

added number_semiring class, plus a few new lemmas;
no changes to the simpset yet

proper case_names for int_cases, int_of_nat_induct;
tuned some proofs, eliminating (cases, auto) anti-pattern;

eliminated Codegen.mode in favour of explicit argument;

tuned headers;

adapted proofs to slightly changed definitions of congruent(2)

constant `contents` renamed to `the_elem`

renamed class/constant eq to equal; tuned some instantiations

diff_minus subsumes diff_def

dropped superfluous [code del]s

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

moved int induction lemma to theory Int as int_bidirectional_induct

moved lemma zdvd_period to theory Int

moved some lemmas from Groebner_Basis here

moved generic lemmas to appropriate places

got rid of [simplified]

use new classes (linordered_)field_inverse_zero

class division_ring_inverse_zero

replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;

added missing mult_1_left to linarith simp rules

now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"

tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)

add more simp rules for Ints

get rid of many duplicate simp rule warnings

modernized structures;

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

separate library theory for type classes combining lattices with various algebraic structures

more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS

streamlined proofs

renamed lemmas "anti_sym" -> "antisym"

modernized structure Reorient_Proc;
explicit merge of constituent functions, avoids exponential blowup when traversing the import graph;
adapted Theory_Data;
tuned;

tuned code setup

moved some dvd [int] facts to Int

moved some dvd [int] facts to Int

moved theory Divides after theory Nat_Numeral; tuned some proof texts

renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"

tuned proofs

added numeral code postprocessor rules on type int

prefer code_inline over code_unfold; use code_unfold_post where appropriate

code attributes use common underscore convention

tuned interface of Lin_Arith

modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs

--HG--
rename : src/HOL/Tools/nat_simprocs.ML => src/HOL/Tools/nat_numeral_simprocs.ML
rename : src/HOL/Tools/int_factor_simprocs.ML => src/HOL/Tools/numeral_simprocs.ML

moved int_factor_simprocs.ML to theory Int

reimplement reorientation simproc using theory data

farewell to class recpower

reorganization of power lemmas

local syntax for Ints; ephermal re-globalization

cleaned up theory power further

power operation defined generic

cleaned up setprod_zero-related lemmas

added setsum_pos_nat

simplify theorem references

no longer delay loading of assoc_fold.ML

distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly

vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement

--HG--
rename : src/HOL/Tools/arith_data.ML => src/HOL/Tools/nat_arith.ML

declare power_Suc [simp]; remove redundant type-specific versions of power_Suc

Merge.

name changes

make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules

declare of_int_number_of_eq [simp]

Added Nitpick tag to 'of_int_of_nat'.
This theorem leads to a more efficient encoding to Kodkod than the definition of 'of_int'.

declare "nat o abs" as default measure for int

added some simp rules

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

stripped Id

no base sort in class import

clean up diff_bin_simps

move all neg-related lemmas to NatBin; make type of neg specific to int

separate neg_simps from rel_simps

revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)

add named lemma lists: neg_simps and iszero_simps

change arith_special simps to avoid using neg

enable eq_bin_simps for simplifying equalities on numerals

enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals

cleaned up subsection headings;
added simp rules for comparisons on binary numbers

made repository layout more coherent with logical distribution structure; stripped some $Id$s

--HG--
rename : src/HOL/Library/Code_Message.thy => src/HOL/Code_Message.thy
rename : src/HOL/Complex/Complex.thy => src/HOL/Complex.thy
rename : src/HOL/Complex/Complex_Main.thy => src/HOL/Complex_Main.thy
rename : src/HOL/Real/ContNotDenum.thy => src/HOL/ContNotDenum.thy
rename : src/HOL/Hyperreal/Deriv.thy => src/HOL/Deriv.thy
rename : src/HOL/Hyperreal/Fact.thy => src/HOL/Fact.thy
rename : src/HOL/Hyperreal/FrechetDeriv.thy => src/HOL/FrechetDeriv.thy
rename : src/HOL/Library/GCD.thy => src/HOL/GCD.thy
rename : src/HOL/Hyperreal/Integration.thy => src/HOL/Integration.thy
rename : src/HOL/Real/Float.thy => src/HOL/Library/Float.thy
rename : src/HOL/Hyperreal/Lim.thy => src/HOL/Lim.thy
rename : src/HOL/Hyperreal/Ln.thy => src/HOL/Ln.thy
rename : src/HOL/Hyperreal/Log.thy => src/HOL/Log.thy
rename : src/HOL/Real/Lubs.thy => src/HOL/Lubs.thy
rename : src/HOL/Hyperreal/MacLaurin.thy => src/HOL/MacLaurin.thy
rename : src/HOL/Hyperreal/NthRoot.thy => src/HOL/NthRoot.thy
rename : src/HOL/Library/Order_Relation.thy => src/HOL/Order_Relation.thy
rename : src/HOL/Real/PReal.thy => src/HOL/PReal.thy
rename : src/HOL/Library/Parity.thy => src/HOL/Parity.thy
rename : src/HOL/Real/RComplete.thy => src/HOL/RComplete.thy
rename : src/HOL/Real/Rational.thy => src/HOL/Rational.thy
rename : src/HOL/Real/Real.thy => src/HOL/Real.thy
rename : src/HOL/Real/RealDef.thy => src/HOL/RealDef.thy
rename : src/HOL/Real/RealPow.thy => src/HOL/RealPow.thy
rename : src/HOL/Hyperreal/Series.thy => src/HOL/Series.thy
rename : src/HOL/Hyperreal/Taylor.thy => src/HOL/Taylor.thy
rename : src/HOL/arith_data.ML => src/HOL/Tools/arith_data.ML
rename : src/HOL/Real/float_arith.ML => src/HOL/Tools/float_arith.ML
rename : src/HOL/Real/float_syntax.ML => src/HOL/Tools/float_syntax.ML
rename : src/HOL/hologic.ML => src/HOL/Tools/hologic.ML
rename : src/HOL/int_arith1.ML => src/HOL/Tools/int_arith.ML
rename : src/HOL/int_factor_simprocs.ML => src/HOL/Tools/int_factor_simprocs.ML
rename : src/HOL/nat_simprocs.ML => src/HOL/Tools/nat_simprocs.ML
rename : src/HOL/Real/rat_arith.ML => src/HOL/Tools/rat_arith.ML
rename : src/HOL/Real/real_arith.ML => src/HOL/Tools/real_arith.ML
rename : src/HOL/simpdata.ML => src/HOL/Tools/simpdata.ML
rename : src/HOL/Hyperreal/Transcendental.thy => src/HOL/Transcendental.thy
rename : src/HOL/Library/RType.thy => src/HOL/Typerep.thy
rename : src/HOL/Library/Univ_Poly.thy => src/HOL/Univ_Poly.thy
rename : src/HOL/Complex/ex/Arithmetic_Series_Complex.thy => src/HOL/ex/Arithmetic_Series_Complex.thy
rename : src/HOL/Complex/ex/BigO_Complex.thy => src/HOL/ex/BigO_Complex.thy
rename : src/HOL/Complex/ex/HarmonicSeries.thy => src/HOL/ex/HarmonicSeries.thy
rename : src/HOL/Complex/ex/MIR.thy => src/HOL/ex/MIR.thy
rename : src/HOL/Complex/ex/ReflectedFerrack.thy => src/HOL/ex/ReflectedFerrack.thy
rename : src/HOL/Complex/ex/Sqrt.thy => src/HOL/ex/Sqrt.thy
rename : src/HOL/Complex/ex/Sqrt_Script.thy => src/HOL/ex/Sqrt_Script.thy
rename : src/HOL/Complex/ex/linrtac.ML => src/HOL/ex/linrtac.ML
rename : src/HOL/Complex/ex/mirtac.ML => src/HOL/ex/mirtac.ML
rename : src/Pure/Tools/quickcheck.ML => src/Tools/quickcheck.ML
rename : src/Pure/Tools/value.ML => src/Tools/value.ML

tuned

slightly tuned

`code func` now just `code`

established canonical argument order in SML code generators

tuned of_nat code generation

non left-linear equations for nbe

added class preorder

code generator setup for "int" also works under eta-contraction

removed some dubious code lemmas

Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
set print_mode and margin appropriately.

Merged theories about wellfoundedness into one: Wellfounded.thy

constant HOL.eq now qualified

moved some code lemmas for Numerals here

removed duplicate lemmas;

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

<= and < on nat no longer depend on wellfounded relations

moved definition of power on ints to theory Int

tuned code setup

joined theories IntDef, Numeral, IntArith to theory Int