Skip to content
Success

Changes

Summary

  1. merged
  2. EXPERIMENTAL replacement of f ` A <= B by f : A -> B in Analysis
Changeset 78249:1260be3f33a4 by paulson:
merged
Changeset 78248:740b23f1138a by paulson _lp15@cam.ac.uk_:
EXPERIMENTAL replacement of f ` A &lt;= B by f : A -&gt; B in Analysis
The file was modified src/HOL/Analysis/Abstract_Metric_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Topological_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Topology_2.thy (diff)
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Fashoda_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.thy (diff)
The file was modified src/HOL/Analysis/Homotopy.thy (diff)
The file was modified src/HOL/Analysis/Lindelof_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Lipschitz.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/Starlike.thy (diff)
The file was modified src/HOL/Analysis/Urysohn.thy (diff)
The file was modified src/HOL/Complex_Analysis/Conformal_Mappings.thy (diff)
The file was modified src/HOL/Complex_Analysis/Riemann_Mapping.thy (diff)
The file was modified src/HOL/Library/FuncSet.thy (diff)