Changes

Summary

added lemmas
merged
Generalising and renaming some basic results
transfer more lemmas
fixed some oversights
avoid duplicate facts, the "trick" was copied without deeper motivation

Changeset 68529:29235951f104 by nipkow: added lemmas
The file was modified	`src/HOL/Rat.thy` (diff)
The file was modified	`src/HOL/Real.thy` (diff)
Changeset 68528:d31e986fbebc by paulson: merged
Changeset 68527:2f4e2aab190a by paulson _lp15@cam.ac.uk_: Generalising and renaming some basic results
The file was modified	`src/HOL/Analysis/Arcwise_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Cauchy_Integral_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Transcendental.thy` (diff)
The file was modified	`src/HOL/Analysis/Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Convex_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Derivative.thy` (diff)
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Great_Picard.thy` (diff)
The file was modified	`src/HOL/Analysis/Henstock_Kurzweil_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Infinite_Products.thy` (diff)
The file was modified	`src/HOL/Analysis/Starlike.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy` (diff)
The file was modified	`src/HOL/Deriv.thy` (diff)
The file was modified	`src/HOL/Fields.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Nonnegative_Real.thy` (diff)
The file was modified	`src/HOL/List.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/NSA.thy` (diff)
The file was modified	`src/HOL/Real.thy` (diff)
The file was modified	`src/HOL/Series.thy` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)
Changeset 68526:f1f989b656bb by immler: transfer more lemmas
The file was modified	`src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy` (diff)
Changeset 68525:e980a0441b61 by immler: fixed some oversights
The file was modified	`src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy` (diff)
Changeset 68524:f5ca4c2157a5 by immler: avoid duplicate facts, the "trick" was copied without deeper motivation
The file was modified	`src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy` (diff)