more rules for natural deduction from inequalities

new lemma

dedicated fact collections for algebraic simplification rules potentially splitting goals

--HG--
extra : rebase_source : ebbd8d0c13409f8fb536c42910e904c24e43dbe6

prefer named lemmas -- more compact proofterms;

official fact collection sign_simps

isabelle update -u path_cartouches;

isabelle update -u control_cartouches;

clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);

suitable logical type class for abs, sgn

--HG--
extra : rebase_source : 27e95dd7f038f114d0cad11ec69599a166229041

add add_eq_0_iff_both_eq_0 and zero_eq_add_iff_both_eq_0 to simp set

--HG--
extra : rebase_source : 61bd5cb95e6c936ef1675a22b0e76e372620d269

more symbols;

misc tuning and modernization;

sharing simp rules between ordered monoids and rings

abstract and concrete multiplicative groups

misc tuning and modernization;

boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes

--HG--
extra : rebase_source : 4542f54b0b7fe6c0bea5be2116706e4cfacadaf0

isabelle update_cartouches -c -t;

more theorems on orderings

--HG--
extra : rebase_source : 4e5a14cb68359f057eb65c380c103e23971ad09c

An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!

generalize more theorems to support enat and ennreal

--HG--
extra : rebase_source : 11176604a37483aa41462153f0aa289df506590d

moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add

--HG--
extra : rebase_source : 8674c79985a670cee921b8193965bb0767549a5c

Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.

--HG--
extra : rebase_source : 54bd3e5fcde04ef38241be91231c48d078b850f2

dropped various legacy fact bindings

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

prefer symbols for "abs";

isabelle update_cartouches -c -t;

Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.

qualifier is mandatory by default;

discontinued specific HTML syntax;

fewer aliases for toplevel theorem statements;

tuned proofs -- less legacy;

eliminated \<Colon>;

new material for multivariate analysis, etc.

isabelle update_cartouches;

explicit commutative additive inverse operation;
more explicit focal point for commutative monoids with an inverse operation

--HG--
extra : rebase_source : ed4c155428dd5783c8e0663805a92b15992e85d3

more canonical order of subscriptions avoids superfluous facts

--HG--
extra : rebase_source : 4626a7762a2840ce4891fcaa6d3121f5f8d7bd20

establish unique preferred fact names

tuned order

--HG--
extra : rebase_source : 3c43f8f9492c8b5c674921fba04cac3d9fb30b78

modernized header uniformly as section;

updated to named_theorems;

reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space

prefer ac_simps collections over separate name bindings for add and mult

reduced name variants for assoc and commute on plus and mult

add mono rules for diff

prefer target-style syntaxx for sublocale

more antiquotations;

fact generalization and name consolidation

more simplification rules on unary and binary minus

--HG--
extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1

killed more "no_atp"s

killed most "no_atp", to make Sledgehammer more complete

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

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

type class for confined subtraction

more explicit Printer.type_emphasis, depending on show_type_emphasis;
tuned signature;

syntax translations always depend on context;

more uniform style for interpretation and sublocale declarations

--HG--
extra : rebase_source : 908fa43d5ac738a6c353d74475cb1910f6a318e8

more explicit show_type_constraint, show_sort_constraint;

typeclass formalising bounded subtraction

prefer ML_file over old uses;

replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones

Groups.thy: generalize several lemmas from class ab_group_add to class group_add

tuned Named_Thms: proper binding;

remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}

special treatment of structure index 1 in Pure, including legacy warning;

move lemma add_eq_0_iff to Groups.thy

discontinued old-style Syntax.constrainC;

typed_print_translation: discontinued show_sorts argument;

moved unparse material to syntax_phases.ML;

added class relation group_add < cancel_semigroup_add

turned show_sorts/show_types into proper configuration options;

use file names relative to master directory of theory source -- Proof General can now handle that due to the ThyLoad.add_path deception (cf. 3ceccd415145);

keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup

discontinued pretending that abel_cancel is logic-independent; cleaned up junk

--HG--
rename : src/Provers/Arith/abel_cancel.ML => src/HOL/Tools/abel_cancel.ML

declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)

dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero

field_simps as named theorems

more localization; tuned proofs

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

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

tuned monoid locales and prefix of sublocale interpretations

added locales for monoids

modernized structure Term_Ord;

more antiquotations;

distributed theory Algebras to theories Groups and Lattices

moved remaning class operations from Algebras.thy to Groups.thy

get rid of many duplicate simp rule warnings

moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy

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