Skip to content
Success

Changes

Summary

  1. merged
  2. tuned Analysis manual
  3. tuned Analysis manual
  4. more rules
  5. tuned material
  6. tuned manual
  7. Removed duplicate theorems from HOL-Analysis
  8. Flattened dependency tree of HOL-Analysis
  9. Merged
  10. Simplified Harmonic_Numbers
  11. Split off new HOL-Complex_Analysis session from HOL-Analysis
Changeset 71199:0aaf16a0f7cc by immler:
merged
Changeset 71198:1bf7d1acbe74 by immler:
tuned Analysis manual
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Metric_Arith.thy (diff)
Changeset 71197:36961c681fed by immler:
tuned Analysis manual
The file was modified src/HOL/Analysis/Analysis.thy (diff)
Changeset 71196:29e7c6d11cf1 by haftmann:
more rules
The file was modified src/HOL/ex/Word.thy (diff)
Changeset 71195:d50a718ccf35 by haftmann:
tuned material
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/Library/Type_Length.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
The file was modified src/HOL/ex/Bit_Operations.thy (diff)
The file was modified src/HOL/ex/Word.thy (diff)
Changeset 71194:26b35a97bddb by nipkow:
tuned manual
The file was modified src/HOL/Analysis/Analysis.thy (diff)
Changeset 71193:777d673fa672 by manuel eberl _eberlm@in.tum.de_:
Removed duplicate theorems from HOL-Analysis
The file was modified src/HOL/Analysis/Retracts.thy (diff)
The file was modified src/HOL/Analysis/Smooth_Paths.thy (diff)
Changeset 71192:a8ccea88b725 by manuel eberl _eberlm@in.tum.de_:
Flattened dependency tree of HOL-Analysis
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Vitali_Covering_Theorem.thy (diff)
Changeset 71190:8b8f9d3b3fac by manuel eberl _eberlm@in.tum.de_:
Simplified Harmonic_Numbers
The file was modified src/HOL/Analysis/Harmonic_Numbers.thy (diff)
Changeset 71189:954ee5acaae0 by manuel eberl _eberlm@in.tum.de_:
Split off new HOL-Complex_Analysis session from HOL-Analysis
The file was addedsrc/HOL/Analysis/Smooth_Paths.thy
The file was addedsrc/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy
The file was addedsrc/HOL/Complex_Analysis/Complex_Analysis.thy
The file was addedsrc/HOL/Complex_Analysis/Conformal_Mappings.thy
The file was addedsrc/HOL/Complex_Analysis/Great_Picard.thy
The file was addedsrc/HOL/Complex_Analysis/Riemann_Mapping.thy
The file was addedsrc/HOL/Complex_Analysis/Winding_Numbers.thy
The file was addedsrc/HOL/Complex_Analysis/document/root.bib
The file was addedsrc/HOL/Complex_Analysis/document/root.tex
The file was modified src/HOL/Analysis/Analysis.thy (diff)
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Complex_Analysis_Basics.thy (diff)
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Analysis/FPS_Convergence.thy (diff)
The file was modified src/HOL/Analysis/Gamma_Function.thy (diff)
The file was modified src/HOL/Analysis/Line_Segment.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Vitali_Covering_Theorem.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/Analysis/Cauchy_Integral_Theorem.thy
The file was removedsrc/HOL/Analysis/Conformal_Mappings.thy
The file was removedsrc/HOL/Analysis/Great_Picard.thy
The file was removedsrc/HOL/Analysis/Winding_Numbers.thy