Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. white space
  2. merged
  3. some fixes connected with card_Diff_singleton
  4. strengthened a few lemmas about finite sets and added a code equation for complex_of_real
Changeset 74226:38c01d7e9f5b by paulson _lp15@cam.ac.uk_:
white space
The file was modified src/HOL/Complex.thy (diff)
Changeset 74225:54b753b90b87 by paulson:
merged
Changeset 74224:e04ec2b9ed97 by paulson _lp15@cam.ac.uk_:
some fixes connected with card_Diff_singleton
The file was modified src/HOL/Analysis/Affine.thy (diff)
The file was modified src/HOL/Quotient_Examples/Quotient_FSet.thy (diff)
Changeset 74223:527088d4a89b by paulson _lp15@cam.ac.uk_:
strengthened a few lemmas about finite sets and added a code equation for complex_of_real
The file was modified src/HOL/Complex.thy (diff)
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Library/Disjoint_Sets.thy (diff)