moved lemmas from AFP

ran isabelle update_op on all sources

more reorganization around sorted_wrt

added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy

proper logical constants

prefer existing logical constant over abbreviation

dropped aliasses

added lemmas demanded by FIXMEs

--HG--
extra : rebase_source : e2ab419767bc144791eca05f3065038591a1bba7

misc tuning and modernization;

prefer [simp] over [iff] as [iff] break HOL-UNITY

add lemmas contributed by Peter Gammie

misc tuning and modernization;

default one-step rules for predicates on relations;
clarified status of legacy input abbreviations

prefer abbreviations for compound operators INFIMUM and SUPREMUM

revisions to limits and derivatives, plus new lemmas

former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";

isabelle update_cartouches -c -t;

add various lemmas

prod_case as canonical name for product type eliminator

tuned proofs -- less legacy;

isabelle update_cartouches;

add lemmas

add lemma

modernized header uniformly as section;

added various facts

typo

prefer plain ASCII / latex over not-so-universal Unicode;

more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)

--HG--
extra : rebase_source : 710314bbc990dc6cb912a800546a75f7c3a07dca

more operations and lemmas

--HG--
extra : rebase_source : 8f5be7e0cdc09c667e66c2cda2c667d4da6e5f73

elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION

killed a few 'metis' calls

renamed '{prod,sum,bool,unit}_case' to 'case_...'

removed theory dependency of BNF_LFP on Datatype

move BNF_LFP up the dependency chain

set_comprehension_pointfree simproc causes to many surprises if enabled by default

rationalize imports

countability of the image of a reflexive transitive closure

killed most "no_atp", to make Sledgehammer more complete

added lemmas and made concerse executable

more converse(p) theorems; tuned proofs;

two useful relation theorems

added lemma

corrected nonsensical associativity of `` and dvd

more relation operations expressed by Finite_Set.fold

a first guess to avoid the Codegenerator_Test to loop infinitely

generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command

define reflp directly, in the manner of symp and transp

dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"

renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")

fixed typo

--HG--
extra : rebase_source : 9faceaa5d14f848f5ee57337e43dc5862026a24d

spelt out missing colemmas

generalized INF_INT_eq, SUP_UN_eq

tuned proofs

tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set

tuned simpset

tuned syntax; more candidates

more fundamental pred-to-set conversions for range and domain by means of inductive_set

--HG--
extra : rebase_source : 62271b2da0fd52b8b598bb504eb41798590b3fa8

more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)

restored accidental omission

--HG--
extra : rebase_source : ce6b28d721d05f6bc75668880dc59ca2f21ee33c

tuned structure

--HG--
extra : rebase_source : ceab636a9cfa6e8738a3cb651a7de9e3e87a8911

tuned structure; dropped already existing syntax declarations

--HG--
extra : rebase_source : 3aff5061aebc337202220f0749aab8c247737823

tuned syntax declarations; tuned structure

--HG--
extra : rebase_source : 1b6c21e91abe00bbf0ca93b6c0f5a24da0bef488

marked candidates for rule declarations

moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy

--HG--
extra : rebase_source : ed15629634477aff0a8efea30547f496c70907ad

explicit remove of lattice notation

moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy

added "'a rel"

cleanup of code declarations

--HG--
extra : rebase_source : 7376929a640011e27309be6654ccf370df37e60a

dropped obsolete code equation for Id

moved acyclic predicate up in hierarchy

--HG--
extra : rebase_source : 4c9a0c3c1dd3de32826493a20016e209648a4e47

modernized definitions

--HG--
extra : rebase_source : d50ecbd4a46b11ec1f49c3eb54ad2ee86a8981ce

tuned specification and lemma distribution among theories; tuned proofs

tuned proofs

observe distinction between sets and predicates more properly

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

adding a definition for refl_on which is friendly for quickcheck and nitpick

adding a nice definition of Id_on for quickcheck and nitpick

added lemmas rel_comp_UNION_distrib(2)

removed semicolons

rule subrelI (for nice Isar proofs of relation inequalities)

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

lemma converse_inv_image

New facts about domain and range in

proper merge of interpretation equations

moved lemma Wellfounded.in_inv_image to Relation.thy

"more standard" argument order of relation composition (op O)

ephermal enforcement of import order to circumvent current problem in merging interpretation morphisms

Merge.

name changes

Moved Order_Relation into Library and moved some of it into Relation.

--HG--
rename : src/HOL/Order_Relation.thy => src/HOL/Library/Order_Relation.thy

changed import hierarchy

added distributivity of relation composition over union [simp]

added lemmas

Added lemmas

integrated FixedPoint into Inductive

ATP blacklisting is now in theory data, attribute noatp

moved lfp_induct2 here

Added simp-rules: "R O {} = {}" and "{} O R = {}"

some new lemmas

more robust syntax for definition/abbreviation/notation;

renamed 'const_syntax' to 'notation';

Changed precedence of "op O" (relation composition) from 60 to 75.

tuned concrete syntax -- abbreviation/const_syntax;

refined 'abbreviation';

Converted translations to abbbreviations.
Removed a few odd functions from Map and AssocList.
Moved chg_map from Map to Bali/Basis.

added many simple lemmas

renamed rules to iprover

new theorem symD

import -> imports

New theory header syntax.

some x-symbols and some new lemmas

converting HOL/UNITY to use unconditional fairness

Removed obsolete function "fun_rel_comp".

removal of blast.overloaded

*** empty log message ***

fixed document;
tuned;

Converted to new theory format.

comp -> rel_comp

moved inv_image to Relation

`` -> and ``` -> ``

^^ -> ```
Univalent -> single_valued

Field of a relation, and some Domain/Range rules

converse: syntax \<inverse>;

*** empty log message ***

Times -> <*>
** -> <*lex*>

renamed Univalent to univalent

tidied using modern infix form

Added some definitions and theorems needed for the
construction of datatypes involving function types.

new preficates refl, sym [from Integ/Equiv], antisym

moved diag (diagonal relation) from Univ to Relation

id <-> Id

inverse -> converse
[It is standard terminology and also used in ZF]

added Univalent

Reduced priority of postfix ^* etc operators such that they are the same as
application. Eg wf r^* now needs to be written wf(r^*).

converse -> ^-1

Simplification and tidying of definitions

Generalized types of some of the operators (thanks to Norbert Voelker)

expanded tabs; renamed subtype to typedef;
incorporated Konrad's changes

Streamlined defs in Relation and added new intro/elim rules to do with
pattern matching in sets: {(x,y). ...} and UN (x,y):A. ...

Trancl is now based on Relation which used to be in Integ.