Changes

Summary

merged
More new theorems, and a necessary correction
A few new theorems
merged
merged
merged
merged
Numerous significant simplifications
stripped unused functionality
tuned

Changeset 77936:041678c7f147 by paulson: merged
Changeset 77935:7f240b0dabd9 by paulson _lp15@cam.ac.uk_: More new theorems, and a necessary correction
The file was modified	`src/HOL/Analysis/Abstract_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Convex_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Further_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Ordered_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Product_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/T1_Spaces.thy` (diff)
The file was modified	`src/HOL/Library/Set_Idioms.thy` (diff)
The file was modified	`src/HOL/Set.thy` (diff)
The file was modified	`src/HOL/Set_Interval.thy` (diff)
Changeset 77934:01c88cf514fc by paulson _lp15@cam.ac.uk_: A few new theorems
The file was modified	`src/HOL/Analysis/Abstract_Limits.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/Archimedean_Field.thy` (diff)
The file was modified	`src/HOL/Conditionally_Complete_Lattices.thy` (diff)
The file was modified	`src/HOL/Fun.thy` (diff)
The file was modified	`src/HOL/Real.thy` (diff)
Changeset 77933:0649ff183dcf by paulson: merged
Changeset 77932:1c7ce7943396 by paulson: merged
Changeset 77931:aca0b615ec4f by paulson: merged
Changeset 77930:84a09beb682d by paulson: merged
Changeset 77929:48aa9928f090 by paulson _lp15@cam.ac.uk_: Numerous significant simplifications
The file was modified	`src/HOL/Analysis/Homotopy.thy` (diff)
Changeset 77928:faaff590bd9e by haftmann: stripped unused functionality
The file was modified	`src/Pure/Isar/code.ML` (diff)
Changeset 77927:f041d5060892 by haftmann: tuned
The file was modified	`src/Tools/Code/code_thingol.ML` (diff)