Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more correct wording
  2. explicit dynamic context for gap-bridging function
  3. more precise NEWS and CONTRIBUTORS
  4. basic documentation for computations
  5. The Great Picard Theorem
  6. New theory about Winding Numbers
  7. new lemmas about segments, etc. Also recast some theorems to use Union rather than general set comprehensions
Changeset 65044:0940a741adf7 by haftmann:
more correct wording
The file was modified src/Doc/Codegen/Computations.thy (diff)
Changeset 65043:fd753468786f by haftmann:
explicit dynamic context for gap-bridging function
The file was modified src/Doc/Codegen/Computations.thy (diff)
The file was modified src/HOL/Decision_Procs/Commutative_Ring.thy (diff)
The file was modified src/HOL/Decision_Procs/Reflective_Field.thy (diff)
The file was modified src/Tools/Code/code_runtime.ML (diff)
Changeset 65042:956ea00a162a by haftmann:
more precise NEWS and CONTRIBUTORS
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
Changeset 65041:2525e680f94f by haftmann:
basic documentation for computations
The file was addedsrc/Doc/Codegen/Computations.thy
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/Doc/Codegen/Adaptation.thy (diff)
The file was modified src/Doc/Codegen/Evaluation.thy (diff)
The file was modified src/Doc/Codegen/Further.thy (diff)
The file was modified src/Doc/Codegen/document/root.tex (diff)
The file was modified src/Doc/Codegen/document/style.sty (diff)
The file was modified src/Doc/ROOT (diff)
Changeset 65040:5975839e8d25 by paulson _lp15@cam.ac.uk_:
The Great Picard Theorem
The file was addedsrc/HOL/Analysis/Great_Picard.thy
The file was modified src/HOL/Analysis/Analysis.thy (diff)
Changeset 65039:87972e6177bc by paulson _lp15@cam.ac.uk_:
New theory about Winding Numbers
The file was addedsrc/HOL/Analysis/Winding_Numbers.thy
The file was modified src/HOL/Analysis/Analysis.thy (diff)
The file was modified src/HOL/Analysis/Conformal_Mappings.thy (diff)
Changeset 65038:9391ea7daa17 by paulson _lp15@cam.ac.uk_:
new lemmas about segments, etc. Also recast some theorems to use Union rather than general set comprehensions
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)