Changes

Summary

merged
support unicode_symbols in input source;
tuned signature;
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies

Changeset 69921:5f67c5e457e3 by wenzelm: merged
Changeset 69920:79c8ff387ed1 by wenzelm: support unicode_symbols in input source;
The file was modified	`src/Pure/PIDE/headless.scala` (diff)
The file was modified	`src/Pure/Tools/dump.scala` (diff)
Changeset 69919:7837309d633a by wenzelm: tuned signature;
The file was modified	`src/Pure/Thy/thy_element.scala` (diff)
Changeset 69918:eddcc7c726f3 by paulson _lp15@cam.ac.uk_: new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
The file was modified	`src/HOL/Analysis/Abstract_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Bounded_Linear_Function.thy` (diff)
The file was modified	`src/HOL/Analysis/Cartesian_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Continuous_Extension.thy` (diff)
The file was modified	`src/HOL/Analysis/Elementary_Metric_Spaces.thy` (diff)
The file was modified	`src/HOL/Analysis/Elementary_Normed_Spaces.thy` (diff)
The file was modified	`src/HOL/Analysis/Finite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Function_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Homotopy.thy` (diff)
The file was modified	`src/HOL/Analysis/Starlike.thy` (diff)
The file was modified	`src/HOL/Analysis/Topology_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Winding_Numbers.thy` (diff)
The file was modified	`src/HOL/Library/Set_Idioms.thy` (diff)
The file was modified	`src/HOL/Limits.thy` (diff)