Changes

Summary

adapting to Isabelle/9aed2da07200
adapting to Isabelle/6bf55e6e0b75

Changeset 7116:d0f58e08c891 by fleury _mathias.fleury@mpi-inf.mpg.de_: adapting to Isabelle/9aed2da07200
The file was modified	`thys/Automatic_Refinement/Lib/Misc.thy` (diff)
The file was modified	`thys/Decreasing-Diagrams/Decreasing_Diagrams.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Misc.thy` (diff)
Changeset 7115:ca3fc19438b8 by fleury _mathias.fleury@mpi-inf.mpg.de_: adapting to Isabelle/6bf55e6e0b75
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi_Real.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Resultant.thy` (diff)
The file was modified	`thys/Cauchy/CauchySchwarz.thy` (diff)
The file was modified	`thys/Cayley_Hamilton/Cayley_Hamilton.thy` (diff)
The file was modified	`thys/Cayley_Hamilton/Square_Matrix.thy` (diff)
The file was modified	`thys/Discrete_Summation/Discrete_Summation.thy` (diff)
The file was modified	`thys/Discrete_Summation/Factorials.thy` (diff)
The file was modified	`thys/Echelon_Form/Rings2.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Conditional_Expectation.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Gouezel_Karlsson.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Kingman.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Measure_Preserving_Transformations.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Product_Topology.thy` (diff)
The file was modified	`thys/Euler_Partition/Euler_Partition.thy` (diff)
The file was modified	`thys/FFT/FFT.thy` (diff)
The file was modified	`thys/Gauss-Jordan-Elim-Fun/Gauss_Jordan_Elim_Fun.thy` (diff)
The file was modified	`thys/Girth_Chromatic/Girth_Chromatic.thy` (diff)
The file was modified	`thys/Integration/Integral.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Determinant.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Kernel.thy` (diff)
The file was modified	`thys/Kleene_Algebra/Matrix.thy` (diff)
The file was modified	`thys/Liouville_Numbers/Liouville_Numbers_Misc.thy` (diff)
The file was modified	`thys/List_Update/BIT.thy` (diff)
The file was modified	`thys/List_Update/BIT_2comp_on2.thy` (diff)
The file was modified	`thys/List_Update/List_Factoring.thy` (diff)
The file was modified	`thys/List_Update/Move_to_Front.thy` (diff)
The file was modified	`thys/Lower_Semicontinuous/Lower_Semicontinuous.thy` (diff)
The file was modified	`thys/Markov_Models/Classifying_Markov_Chain_States.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Crowds_Protocol.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Gossip_Broadcast.thy` (diff)
The file was modified	`thys/Markov_Models/ex/PCTL.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy` (diff)
The file was modified	`thys/Perfect-Number-Thm/PerfectBasics.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Perron_Frobenius.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Gauss_Lemma.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Square_Free_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom_Poly.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Language_Semantics.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Trace_Based.thy` (diff)
The file was modified	`thys/QR_Decomposition/Generalizations2.thy` (diff)
The file was modified	`thys/Random_Graph_Subgraph_Threshold/Ugraph_Misc.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/SD_Efficiency.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Stochastic_Dominance.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Utility_Functions.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Generalizations.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Miscellaneous.thy` (diff)
The file was modified	`thys/Rep_Fin_Groups/Rep_Fin_Groups.thy` (diff)
The file was modified	`thys/Secondary_Sylow/GroupAction.thy` (diff)
The file was modified	`thys/Stirling_Formula/Stirling_Formula.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Lib/Misc_Polynomial.thy` (diff)
The file was modified	`thys/Sturm_Tarski/Sturm_Tarski.thy` (diff)
The file was modified	`thys/Tarskis_Geometry/Linear_Algebra2.thy` (diff)
The file was modified	`thys/Tarskis_Geometry/Miscellany.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Up_Down.thy` (diff)
The file was modified	`thys/pGCL/Determinism.thy` (diff)
The file was modified	`thys/pGCL/Healthiness.thy` (diff)
The file was modified	`thys/pGCL/Sublinearity.thy` (diff)