Changes

Summary

more ambitious test;
added lemmas and tuned proofs
merged
Switching to inverse image and constant_on, plus some new material

Changeset 66887:72b78ee82f7b by wenzelm: more ambitious test;
The file was modified	`src/Pure/Admin/isabelle_cronjob.scala` (diff)
Changeset 66886:960509bfd47e by haftmann: added lemmas and tuned proofs
The file was modified	`src/HOL/Code_Numeral.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Normalized_Fraction.thy` (diff)
The file was modified	`src/HOL/Divides.thy` (diff)
The file was modified	`src/HOL/Euclidean_Division.thy` (diff)
The file was modified	`src/HOL/Int.thy` (diff)
The file was modified	`src/HOL/Library/Numeral_Type.thy` (diff)
The file was modified	`src/HOL/Word/Word_Miscellaneous.thy` (diff)
Changeset 66885:d3d508b23d1d by paulson: merged
Changeset 66884:c2128ab11f61 by paulson _lp15@cam.ac.uk_: Switching to inverse image and constant_on, plus some new material
The file was modified	`src/HOL/Analysis/Brouwer_Fixpoint.thy` (diff)
The file was modified	`src/HOL/Analysis/Cauchy_Integral_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Conformal_Mappings.thy` (diff)
The file was modified	`src/HOL/Analysis/Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Continuous_Extension.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/Henstock_Kurzweil_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Homeomorphism.thy` (diff)
The file was modified	`src/HOL/Analysis/Jordan_Curve.thy` (diff)
The file was modified	`src/HOL/Analysis/Path_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Starlike.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/Winding_Numbers.thy` (diff)