Skip to content
Success

Changes

Summary

  1. move FuncSet back to HOL-Library (amending 493b818e8e10)
Changeset 68188:2af1f142f855 by immler:
move FuncSet back to HOL-Library (amending 493b818e8e10)
The file was addedsrc/HOL/Library/FuncSet.thy
The file was modified src/HOL/Algebra/Congruence.thy (diff)
The file was modified src/HOL/Algebra/Group.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Analysis/Sigma_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/Metis_Examples/Abstraction.thy (diff)
The file was modified src/HOL/Metis_Examples/Tarski.thy (diff)
The file was modified src/HOL/Number_Theory/Prime_Powers.thy (diff)
The file was modified src/HOL/Vector_Spaces.thy (diff)
The file was modified src/HOL/ex/Ballot.thy (diff)
The file was modified src/HOL/ex/Birthday_Paradox.thy (diff)
The file was modified src/HOL/ex/Tarski.thy (diff)
The file was removedsrc/HOL/FuncSet.thy