SuccessChanges

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. merged
  2. reverted the substitution here
  3. merged
  4. fixed some remarkably ugly proofs
  5. de-applying and tidying
Changeset 72305:6f0e85e16d84 by paulson:
merged
Changeset 72304:6fdeef6d6335 by paulson _lp15@cam.ac.uk_:
reverted the substitution here
The file was modifiedsrc/HOL/Library/Permutations.thy
Changeset 72303:4e649ea1f76b by paulson:
merged
Changeset 72302:d7d90ed4c74e by paulson _lp15@cam.ac.uk_:
fixed some remarkably ugly proofs
The file was modifiedsrc/HOL/Analysis/Brouwer_Fixpoint.thy
The file was modifiedsrc/HOL/Analysis/Polytope.thy
The file was modifiedsrc/HOL/Analysis/Simplex_Content.thy
The file was modifiedsrc/HOL/Analysis/Starlike.thy
The file was modifiedsrc/HOL/Binomial.thy
The file was modifiedsrc/HOL/Finite_Set.thy
The file was modifiedsrc/HOL/Library/FSet.thy
The file was modifiedsrc/HOL/Library/Infinite_Set.thy
The file was modifiedsrc/HOL/Library/Perm.thy
The file was modifiedsrc/HOL/Library/Permutations.thy
The file was modifiedsrc/HOL/List.thy
The file was modifiedsrc/HOL/Number_Theory/Quadratic_Reciprocity.thy
The file was modifiedsrc/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy
The file was modifiedsrc/HOL/Set_Interval.thy
The file was modifiedsrc/HOL/Vector_Spaces.thy
Changeset 72301:c5d1a01d2d6c by paulson _lp15@cam.ac.uk_:
de-applying and tidying
The file was modifiedsrc/HOL/Analysis/Complex_Transcendental.thy

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. fixed proofs — not sure why they were failing
  2. removal of some theorem aliases involving "card"
Changeset 11320:a74ae3b9abd2 by paulson _lp15@cam.ac.uk_:
fixed proofs — not sure why they were failing
The file was modifiedthys/Winding_Number_Eval/Winding_Number_Eval.thy
Changeset 11319:b27be6381657 by paulson _lp15@cam.ac.uk_:
removal of some theorem aliases involving "card"
The file was modifiedthys/Auto2_HOL/HOL/Set_Thms.thy
The file was modifiedthys/Bondy/Bondy.thy
The file was modifiedthys/Card_Multisets/Card_Multisets.thy
The file was modifiedthys/Card_Number_Partitions/Card_Number_Partitions.thy
The file was modifiedthys/Card_Partitions/Card_Partitions.thy
The file was modifiedthys/Chandy_Lamport/Example.thy
The file was modifiedthys/Chandy_Lamport/Snapshot.thy
The file was modifiedthys/Complex_Geometry/More_Set.thy
The file was modifiedthys/Consensus_Refined/MRU/CT_Proofs.thy
The file was modifiedthys/Consensus_Refined/MRU/Paxos_Proofs.thy
The file was modifiedthys/CoreC++/Execute.thy
The file was modifiedthys/Count_Complex_Roots/More_Polynomials.thy
The file was modifiedthys/Extended_Finite_State_Machines/FSet_Utils.thy
The file was modifiedthys/Factored_Transition_System_Bounding/FactoredSystem.thy
The file was modifiedthys/Gauss_Jordan/System_Of_Equations.thy
The file was modifiedthys/Gauss_Sums/Gauss_Sums.thy
The file was modifiedthys/Generic_Join/Examples_Join.thy
The file was modifiedthys/Generic_Join/Generic_Join.thy
The file was modifiedthys/Generic_Join/Generic_Join_Correctness.thy
The file was modifiedthys/Graph_Saturation/MissingRelation.thy
The file was modifiedthys/Groebner_Macaulay/Cone_Decomposition.thy
The file was modifiedthys/Groebner_Macaulay/Dube_Prelims.thy
The file was modifiedthys/Gromov_Hyperbolicity/Isometries.thy
The file was modifiedthys/Interval_Arithmetic_Word32/Finite_String.thy
The file was modifiedthys/Jordan_Normal_Form/DL_Missing_Sublist.thy
The file was modifiedthys/Jordan_Normal_Form/Missing_Permutations.thy
The file was modifiedthys/Koenigsberg_Friendship/FriendshipTheory.thy
The file was modifiedthys/Koenigsberg_Friendship/MoreGraph.thy
The file was modifiedthys/Kuratowski_Closure_Complement/KuratowskiClosureComplementTheorem.thy
The file was modifiedthys/LOFT/OpenFlow_Helpers.thy
The file was modifiedthys/Latin_Square/Latin_Square.thy
The file was modifiedthys/Linear_Inequalities/Missing_VS_Connect.thy
The file was modifiedthys/List-Infinite/CommonSet/SetInterval2.thy
The file was modifiedthys/Locally-Nameless-Sigma/Sigma/Sigma.thy
The file was modifiedthys/MFMC_Countable/Max_Flow_Min_Cut_Countable.thy
The file was modifiedthys/Matroids/Matroid.thy
The file was modifiedthys/Menger/Menger.thy
The file was modifiedthys/Menger/MengerInduction.thy
The file was modifiedthys/Neumann_Morgenstern_Utility/Lotteries.thy
The file was modifiedthys/Orbit_Stabiliser/Tetrahedron.thy
The file was modifiedthys/Ordinal_Partitions/Omega_Omega.thy
The file was modifiedthys/Partial_Order_Reduction/Extensions/ESet_Extensions.thy
The file was modifiedthys/Polynomials/MPoly_Type_Class_Ordered.thy
The file was modifiedthys/Probabilistic_System_Zoo/Bool_Bounded_Set.thy
The file was modifiedthys/Probabilistic_System_Zoo/Finitely_Bounded_Set_Counterexample.thy
The file was modifiedthys/Projective_Geometry/Desargues_2D.thy
The file was modifiedthys/Propositional_Proof_Systems/Sema_Craig.thy
The file was modifiedthys/QHLProver/Grover.thy
The file was modifiedthys/QHLProver/Partial_State.thy
The file was modifiedthys/Random_Graph_Subgraph_Threshold/Ugraph_Misc.thy
The file was modifiedthys/Secondary_Sylow/GroupAction.thy
The file was modifiedthys/Secondary_Sylow/SndSylow.thy
The file was modifiedthys/SenSocialChoice/FSext.thy
The file was modifiedthys/Smith_Normal_Form/Cauchy_Binet.thy
The file was modifiedthys/Smith_Normal_Form/SNF_Missing_Lemmas.thy
The file was modifiedthys/Smith_Normal_Form/SNF_Uniqueness.thy
The file was modifiedthys/Symmetric_Polynomials/Symmetric_Polynomials.thy
The file was modifiedthys/Tarskis_Geometry/Miscellany.thy
The file was modifiedthys/Tree_Decomposition/TreewidthCompleteGraph.thy
The file was modifiedthys/Tree_Decomposition/TreewidthTree.thy
The file was modifiedthys/Twelvefold_Way/Card_Bijections.thy
The file was modifiedthys/Twelvefold_Way/Preliminaries.thy
The file was modifiedthys/Vickrey_Clarke_Groves/MiscTools.thy
The file was modifiedthys/Vickrey_Clarke_Groves/RelationProperties.thy
The file was modifiedthys/Vickrey_Clarke_Groves/SetUtils.thy
The file was modifiedthys/WOOT_Strong_Eventual_Consistency/Sorting.thy