Changes

Summary

tuned proof
eliminated irregular aliasses
avoid references to lemmas designed for prover tools
eliminated irregular aliasses
more standardized theorem names for facts involving the div and mod identity
more standardized names

Changeset 7204:c15cf57f0f67 by haftmann: tuned proof
The file was modified	`thys/Hermite/Hermite.thy` (diff)
Changeset 7203:76678d07bcb3 by haftmann: eliminated irregular aliasses
The file was modified	`thys/AutoFocus-Stream/AF_Stream.thy` (diff)
The file was modified	`thys/AutoFocus-Stream/ListSlice.thy` (diff)
The file was modified	`thys/Consensus_Refined/Consensus_Misc.thy` (diff)
The file was modified	`thys/Group-Ring-Module/Algebra4.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/BinOp.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/Cooper.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/Markov_Models/Classifying_Markov_Chain_States.thy` (diff)
The file was modified	`thys/Nat-Interval-Logic/IL_Interval.thy` (diff)
The file was modified	`thys/Nat-Interval-Logic/IL_IntervalOperators.thy` (diff)
The file was modified	`thys/Native_Word/Word_Misc.thy` (diff)
The file was modified	`thys/Presburger-Automata/Presburger_Automata.thy` (diff)
The file was modified	`thys/Word_Lib/More_Divides.thy` (diff)
The file was modified	`thys/Word_Lib/Word_Lemmas.thy` (diff)
Changeset 7202:41c57c1e1ea3 by haftmann: avoid references to lemmas designed for prover tools
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Newton_Interpolation.thy` (diff)
The file was modified	`thys/RSAPSS/EMSAPSS.thy` (diff)
The file was modified	`thys/RSAPSS/RSAPSS.thy` (diff)
Changeset 7201:43ab9501f6d1 by haftmann: eliminated irregular aliasses
The file was modified	`thys/AutoFocus-Stream/IL_AF_Stream_Exec.thy` (diff)
The file was modified	`thys/AutoFocus-Stream/ListSlice.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Lib/Misc.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Gouezel_Karlsson.thy` (diff)
The file was modified	`thys/List-Infinite/CommonArith/Util_Div.thy` (diff)
The file was modified	`thys/List_Update/OPT2.thy` (diff)
The file was modified	`thys/Matrix_Tensor/Matrix_Tensor.thy` (diff)
The file was modified	`thys/Native_Word/Word_Misc.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/PRecFun.thy` (diff)
The file was modified	`thys/TortoiseHare/TortoiseHare.thy` (diff)
Changeset 7200:0cb455106d79 by haftmann: more standardized theorem names for facts involving the div and mod identity
The file was modified	`thys/AutoFocus-Stream/IL_AF_Stream_Exec.thy` (diff)
The file was modified	`thys/AutoFocus-Stream/ListSlice.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Lib/Misc.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy` (diff)
The file was modified	`thys/Consensus_Refined/Consensus_Misc.thy` (diff)
The file was modified	`thys/Consensus_Refined/MRU/Three_Steps.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Gouezel_Karlsson.thy` (diff)
The file was modified	`thys/Ergodic_Theory/SG_Library_Complement.thy` (diff)
The file was modified	`thys/FileRefinement/FileRefinement.thy` (diff)
The file was modified	`thys/Formula_Derivatives/Abstract_Formula.thy` (diff)
The file was modified	`thys/Formula_Derivatives/Presburger_Formula.thy` (diff)
The file was modified	`thys/Group-Ring-Module/Algebra3.thy` (diff)
The file was modified	`thys/Hermite/Hermite.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/BinOp.thy` (diff)
The file was modified	`thys/Knot_Theory/Kauffman_Matrix.thy` (diff)
The file was modified	`thys/List-Infinite/CommonArith/Util_Div.thy` (diff)
The file was modified	`thys/List_Update/BIT_2comp_on2.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/Pi_Regular_Operators.thy` (diff)
The file was modified	`thys/Matrix_Tensor/Matrix_Tensor.thy` (diff)
The file was modified	`thys/Native_Word/Word_Misc.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Dvd_Int_Poly.thy` (diff)
The file was modified	`thys/RSAPSS/EMSAPSS.thy` (diff)
The file was modified	`thys/RSAPSS/Word.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/PRecFinSet.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/PRecFun.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Impl/IICF_Array_Matrix.thy` (diff)
The file was modified	`thys/Sqrt_Babylonian/NthRoot_Impl.thy` (diff)
The file was modified	`thys/Sqrt_Babylonian/Sqrt_Babylonian_Auxiliary.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Sturm_Theorem.thy` (diff)
The file was modified	`thys/Sturm_Tarski/Sturm_Tarski.thy` (diff)
The file was modified	`thys/Word_Lib/Aligned.thy` (diff)
The file was modified	`thys/Word_Lib/HOL_Lemmas.thy` (diff)
The file was modified	`thys/Word_Lib/Word_Lemmas.thy` (diff)
Changeset 7199:8760a0051f56 by haftmann: more standardized names
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Resultant.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Reconstruction.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Square_Free_Factorization_Int.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Square_Free_Int_To_Square_Free_GFp.thy` (diff)
The file was modified	`thys/Cartan_FP/Cartan.thy` (diff)
The file was modified	`thys/Consensus_Refined/Consensus_Misc.thy` (diff)
The file was modified	`thys/Descartes_Sign_Rule/Descartes_Sign_Rule.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Ergodicity.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Gouezel_Karlsson.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Product_Topology.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Recurrence.thy` (diff)
The file was modified	`thys/Euler_Partition/Euler_Partition.thy` (diff)
The file was modified	`thys/Hermite/Hermite.thy` (diff)
The file was modified	`thys/IEEE_Floating_Point/IEEE_Properties.thy` (diff)
The file was modified	`thys/Impossible_Geometry/Impossible_Geometry.thy` (diff)
The file was modified	`thys/Knot_Theory/Kauffman_Matrix.thy` (diff)
The file was modified	`thys/Matrix_Tensor/Matrix_Tensor.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/One_Step_Method.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Order_Polynomial.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Polynomial_Divisibility.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Square_Free_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Newton_Interpolation.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Language_Semantics.thy` (diff)
The file was modified	`thys/QR_Decomposition/QR_Decomposition.thy` (diff)
The file was modified	`thys/Sqrt_Babylonian/Sqrt_Babylonian_Auxiliary.thy` (diff)
The file was modified	`thys/Stern_Brocot/Stern_Brocot_Tree.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Lib/Misc_Polynomial.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Sturm_Theorem.thy` (diff)
The file was modified	`thys/Sturm_Tarski/Sturm_Tarski.thy` (diff)
The file was modified	`thys/Tarskis_Geometry/Hyperbolic_Tarski.thy` (diff)
The file was modified	`thys/Word_Lib/Word_Lemmas.thy` (diff)