Skip to content
Success

Changes

Summary

  1. merged
  2. tuned Analysis/Analysis;
  3. characterization of typical bit operations
  4. merged
  5. renamed Analysis/Winding_Numbers to Winding_Numbers_2; reorganised Analysis/Cauchy_Integral_Theorem by splitting it into Contour_Integration, Winding_Numbers,Cauchy_Integral_Theorem and Cauchy_Integral_Formula.
  6. transfer rule for bit operation
  7. characterization of singleton bit operation
Changeset 71187:758a9f944783 by wenda li _wl302@cam.ac.uk_:
tuned Analysis/Analysis;
The file was modified src/HOL/Analysis/Analysis.thy (diff)
Changeset 71186:3d35e12999ba by haftmann:
characterization of typical bit operations
The file was modified src/HOL/ex/Bit_Operations.thy (diff)
The file was modified src/HOL/ex/Word.thy (diff)
Changeset 71184:d62fdaafdafc by wenda li _wl302@cam.ac.uk_:
renamed Analysis/Winding_Numbers to Winding_Numbers_2; reorganised Analysis/Cauchy_Integral_Theorem by splitting it into Contour_Integration, Winding_Numbers,Cauchy_Integral_Theorem and Cauchy_Integral_Formula.
The file was addedsrc/HOL/Analysis/Cauchy_Integral_Formula.thy
The file was addedsrc/HOL/Analysis/Contour_Integration.thy
The file was addedsrc/HOL/Analysis/Winding_Numbers_2.thy
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Analysis/Conformal_Mappings.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Retracts.thy (diff)
The file was modified src/HOL/Analysis/Winding_Numbers.thy (diff)
Changeset 71183:eda1ef0090ef by haftmann:
transfer rule for bit operation
The file was modified src/HOL/ex/Word.thy (diff)
Changeset 71182:410935efbf5c by haftmann:
characterization of singleton bit operation
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
The file was modified src/HOL/Transfer.thy (diff)
The file was modified src/HOL/ex/Word.thy (diff)