avoid pending shyps in global theory facts;

added lemmas

removed duplicates

dedicated definition for coprimality

--HG--
extra : rebase_source : 891168c98ce62efae6b7e72c7d3365fea12b33ae

abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel

--HG--
extra : rebase_source : c6612d6016d811043143eafb7a671631287494a1

theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;

--HG--
rename : src/HOL/Main.thy => src/HOL/Pre_Main.thy

moved some lemmas to appropriate places

--HG--
extra : rebase_source : d3d8537b1c25edc3e07620dda770ad1feb37ea72

A few new lemmas and needed adaptations

setprod -> prod

setsum -> sum

more standardized names

tuned proofs;

more complete simpset for linear arithmetic to avoid warnings: terms such as (2x + 2y)/2 can then be simplified by the linear arithmetic prover during its proof replay

misc tuning and modernization;

Tuned looping simp rules in semiring_div

--HG--
extra : rebase_source : 3b3829fdddfdfffaad7cac785a601ef678dc9b93

misc tuning and modernization;

more canonical names

dropped various legacy fact bindings

more complete setup for 'Rat' in Nitpick

prefer symbols for "abs";

prefer symbols for "floor", "ceiling";

isabelle update_cartouches -c -t;

simplified simproc programming interfaces;

prefer symbols;

isabelle update_cartouches;

avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead

uniform _ div _ as infix syntax for ring division

--HG--
extra : rebase_source : c4a1892078772c7ce9af33ad66e2abfefe7adea9

separate class for division operator, with particular syntax added in more specific classes

conversion between division on nat/int and division in archmedean fields

given up separate type classes demanding `inverse 0 = 0`

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

import general theorems from AFP/Markov_Models

modernized header uniformly as section;

more simp rules concerning dvd and even/odd

--HG--
extra : rebase_source : 895ed3f871c22790e8d199a30828e91bc13bd735

explicit separation of signed and unsigned numerals using existing lexical categories num and xnum

more appropriate postprocessing of rational numbers: extract sign to front of fraction

prefer ac_simps collections over separate name bindings for add and mult

reduced name variants for assoc and commute on plus and mult

moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin

--HG--
extra : rebase_source : cd4a9d91f2d415deaa6fd3411b5402ef770d74d2

must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure

added divide_nonneg_nonneg and co; made it a simp rule

--HG--
extra : rebase_source : 998eadb7cfbf8720cf961ac2e149ce4537557a47

made mult_pos_pos a simp rule

revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules

removing simprule status for divide_minus_left and divide_minus_right

more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;

explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;

prefer more canonical names for lemmas on min/max

eliminiated neg_numeral in favour of - (numeral _)

support of_rat with 0 or 1 on order relations

more simplification rules on unary and binary minus

--HG--
extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1

use lifting_forget for deregistering numeric types as a quotient type

tuned proofs -- clarified flow of facts wrt. calculation;

standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;

move Lifting/Transfer relevant parts of Library/Quotient_* to Main

tuned;

better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal

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

reform of predicate compiler / quickcheck theories:
implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers!
avoid odd New_ prefix by joining related theories;
avoid overcompact name DSequence;
separated predicate inside random monad into separate theory;
consolidated name of theory Quickcheck

--HG--
rename : src/HOL/DSequence.thy => src/HOL/Limited_Sequence.thy
rename : src/HOL/Quickcheck.thy => src/HOL/Quickcheck_Random.thy
extra : rebase_source : b6adaac1637d6d1cc809d2f937ae890fcc21969c

add quotient_of_div

--HG--
extra : rebase_source : 6927ab046fdc2bf74173dc2e2b5f06fc5e3c2897

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

prefer ML_file over old uses;

use quot_del instead of ML code in Rat.thy

simplify instance proofs for rat

--HG--
extra : transplant_source : %A4%AC%BA%89%85%90%97%16%EDf%13L%3B3%A7%AE%89%A8p%07

convert Rat.thy to use lift_definition/transfer

merged fork with new numeral representation (see NEWS)

choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing

hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;

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

improved generators for rational numbers to generate negative numbers;
added examples

remove unsound line in Nitpick's "rat" setup

removing old code generator setup for rational numbers; tuned

adding code equations for partial_term_of for rational numbers

adding narrowing instances for real and rational

adding code equations to execute floor and ceiling on rational and real numbers

adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)

rational and real instances for new compilation scheme for exhaustive quickcheck

moving exhaustive_generators.ML to Quickcheck directory

--HG--
rename : src/HOL/Tools/exhaustive_generators.ML => src/HOL/Tools/Quickcheck/exhaustive_generators.ML

renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics

adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real

adapted proofs to slightly changed definitions of congruent(2)

replaced slightly odd locale congruent by plain definition

equivI has replaced equiv.intro

constant `contents` renamed to `the_elem`

renamed class/constant eq to equal; tuned some instantiations

replace "setup" with "declaration"

adapt occurrences of renamed Nitpick functions

nicer xsymbol syntax for fcomp and scomp

adjust Nitpick's handling of "<" on "rat"s and "reals"

constant Rat.normalize needs to be qualified;

explicit is better than implicit

use new classes (linordered_)field_inverse_zero

class division_ring_inverse_zero

separated instantiation of division_by_zero

user interface for abstract datatypes is an attribute, not a command

tuned prefixes of ac interpretations

clarified @{const_name} vs. @{const_abbrev};

implement quotient_of for odl SML code generator

bound argument for abstype proposition

renamed theory Rational to Rat

--HG--
rename : src/HOL/Rational.thy => src/HOL/Rat.thy