Skip to content
Aborted

Changes

Summary

  1. Deleted problematic code equation in Codegenerator_Test
  2. Merge
  3. New theory for Homeomorphisms
  4. Merge
  5. renamings and new material
  6. new theorem
  7. deleted stray thm command
  8. deleted needless comment
  9. Resolved cyclic dependency of theories
  10. Merged
  11. Added set permutations/random permutations
Changeset 63132:8230358fab88 by eberlm:
Deleted problematic code equation in Codegenerator_Test
The file was modified src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy (diff)
The file was modified src/HOL/Number_Theory/Factorial_Ring.thy (diff)
The file was modified src/HOL/Probability/Random_Permutations.thy (diff)
Changeset 63130:4ae5da02d627 by paulson _lp15@cam.ac.uk_:
New theory for Homeomorphisms
The file was addedsrc/HOL/Multivariate_Analysis/Homeomorphism.thy
Changeset 63128:24708cf4ba61 by paulson _lp15@cam.ac.uk_:
renamings and new material
The file was modified src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Derivative.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
Changeset 63127:360d9997fac9 by paulson _lp15@cam.ac.uk_:
new theorem
The file was modified src/HOL/Library/Countable_Set.thy (diff)
Changeset 63126:2b50f79829d2 by paulson _lp15@cam.ac.uk_:
deleted stray thm command
The file was modified src/HOL/Multivariate_Analysis/Path_Connected.thy (diff)
Changeset 63125:f2d3f8427bc2 by paulson _lp15@cam.ac.uk_:
deleted needless comment
The file was modified src/HOL/Multivariate_Analysis/Path_Connected.thy (diff)
Changeset 63124:6a17bcddd6c2 by eberlm:
Resolved cyclic dependency of theories
The file was modified src/HOL/Probability/Random_Permutations.thy (diff)
Changeset 63123:b29a8f57e3a0 by eberlm:
Merged
Changeset 63122:dd651e3f7413 by eberlm:
Added set permutations/random permutations
The file was addedsrc/HOL/Library/Set_Permutations.thy
The file was addedsrc/HOL/Probability/Random_Permutations.thy
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/Probability/Probability.thy (diff)