Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. fixed markup
  2. ignore isolated nodes by default;
  3. merged
  4. cycle check with informative error;
  5. tuned: each session has at most one defining entry;
  6. more operations;
  7. tuned signature;
  8. tuned signature;
  9. Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
  10. Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.
Changeset 66835:ecc99a5a1ab8 by paulson _lp15@cam.ac.uk_:
fixed markup
The file was modified src/HOL/Analysis/Connected.thy (diff)
Changeset 66834:c925393ae6b9 by wenzelm:
ignore isolated nodes by default;
The file was modified src/Pure/General/graph_display.scala (diff)
Changeset 66833:091012ac3dc2 by wenzelm:
merged
Changeset 66832:875fe2cb7e70 by wenzelm:
cycle check with informative error;
The file was modified src/Pure/Admin/afp.scala (diff)
Changeset 66831:29ea2b900a05 by wenzelm:
tuned: each session has at most one defining entry;
The file was modified src/Pure/Admin/afp.scala (diff)
Changeset 66830:3b50269b90c2 by wenzelm:
more operations;
The file was modified src/Pure/General/graph.ML (diff)
The file was modified src/Pure/General/graph.scala (diff)
Changeset 66829:5baca4c94737 by wenzelm:
tuned signature;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 66828:3c936ebebc23 by wenzelm:
tuned signature;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 66827:c94531b5007d by paulson _lp15@cam.ac.uk_:
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
The file was addedsrc/HOL/Analysis/Connected.thy
The file was modified src/HOL/Analysis/Bounded_Linear_Function.thy (diff)
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Complex_Analysis_Basics.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/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Function_Topology.thy (diff)
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
The file was modified src/HOL/Analysis/Great_Picard.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.thy (diff)
The file was modified src/HOL/Analysis/Ordered_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Riemann_Mapping.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Uniform_Limit.thy (diff)
The file was modified src/HOL/Analysis/Winding_Numbers.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HLim.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
Changeset 66826:0d60d2118544 by paulson _lp15@cam.ac.uk_:
Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.
The file was addedsrc/HOL/Analysis/Riemann_Mapping.thy
The file was modified NEWS (diff)
The file was modified src/HOL/Analysis/Analysis.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Winding_Numbers.thy (diff)