Changes

Summary

merged
reoriented congruence rules in non-explosive direction
more fine-grained type class hierarchy for div and mod
clarified prefix
standardized notation
absorbed into Main HOL

Changeset 7508:38d931b6990e by haftmann: merged
Changeset 7507:3097e1db9887 by haftmann: reoriented congruence rules in non-explosive direction
The file was modified	`thys/AutoFocus-Stream/IL_AF_Stream.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod_Finite_Field.thy` (diff)
The file was modified	`thys/Euler_Partition/Euler_Partition.thy` (diff)
The file was modified	`thys/Formula_Derivatives/Presburger_Formula.thy` (diff)
The file was modified	`thys/Heard_Of/ute/UteProof.thy` (diff)
The file was modified	`thys/Hermite/Hermite.thy` (diff)
The file was modified	`thys/IP_Addresses/NumberWang_IPv4.thy` (diff)
The file was modified	`thys/Lehmer/Lehmer.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/QEpres.thy` (diff)
The file was modified	`thys/List-Infinite/CommonArith/Util_Div.thy` (diff)
The file was modified	`thys/Nat-Interval-Logic/IL_Interval.thy` (diff)
The file was modified	`thys/Native_Word/Word_Misc.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Graph_Genus.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Prime_Factorization.thy` (diff)
The file was modified	`thys/Pratt_Certificate/Pratt_Certificate.thy` (diff)
The file was modified	`thys/Presburger-Automata/Presburger_Automata.thy` (diff)
The file was modified	`thys/RSAPSS/Cryptinverts.thy` (diff)
The file was modified	`thys/RSAPSS/Mod.thy` (diff)
The file was modified	`thys/RSAPSS/Wordarith.thy` (diff)
The file was modified	`thys/Word_Lib/Word_Lemmas.thy` (diff)
Changeset 7506:db97f3eb1839 by haftmann: more fine-grained type class hierarchy for div and mod
The file was modified	`thys/Sturm_Sequences/Sturm_Theorem.thy` (diff)
Changeset 7505:3e9fb7b3becb by haftmann: clarified prefix
The file was modified	`thys/Berlekamp_Zassenhaus/Square_Free_Factorization_Int.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Polynomial_Division.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Polynomial.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom_Poly.thy` (diff)
Changeset 7504:8f153c64b874 by haftmann: standardized notation
The file was modified	`thys/Automatic_Refinement/Lib/Misc.thy` (diff)
The file was modified	`thys/Binomial-Heaps/BinomialHeap.thy` (diff)
The file was modified	`thys/Binomial-Heaps/SkewBinomialHeap.thy` (diff)
The file was modified	`thys/Decreasing-Diagrams/Decreasing_Diagrams.thy` (diff)
The file was modified	`thys/Jordan_Hoelder/CompositionSeries.thy` (diff)
The file was modified	`thys/Jordan_Hoelder/JordanHolder.thy` (diff)
The file was modified	`thys/Jordan_Hoelder/SndIsomorphismGrp.thy` (diff)
The file was modified	`thys/Jordan_Hoelder/SubgroupsAndNormalSubgroups.thy` (diff)
The file was modified	`thys/Nested_Multisets_Ordinals/Nested_Multiset.thy` (diff)
The file was modified	`thys/Nested_Multisets_Ordinals/Signed_Multiset.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/ConstraintSystems.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Misc.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Semantics.thy` (diff)
The file was modified	`thys/Secondary_Sylow/SndSylow.thy` (diff)
The file was modified	`thys/Secondary_Sylow/SubgroupConjugation.thy` (diff)
The file was modified	`thys/SuperCalc/multisets_continued.thy` (diff)
The file was modified	`thys/SuperCalc/superposition.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/Multiset_Extension.thy` (diff)
Changeset 7503:ea25f88c7bf6 by haftmann: absorbed into Main HOL
The file was modified	`thys/Polynomial_Interpolation/Missing_Unsorted.thy` (diff)