Changes

Summary

export in foundational order;
recovered HOL-Proofs-Lambda from 8aedca31957d: avoid problems with program extraction according to d136af442665;
more Pure theory content;
Small lemmas about analysis
merged
de-applying

Changeset 68724:7fafadbf16c7 by wenzelm: export in foundational order;
The file was modified	`src/Pure/Thy/export_theory.ML` (diff)
Changeset 68723:60611540bcff by wenzelm: recovered HOL-Proofs-Lambda from 8aedca31957d: avoid problems with program extraction according to d136af442665;
The file was modified	`src/HOL/List.thy` (diff)
Changeset 68722:6aea897bff2a by wenzelm: more Pure theory content;
The file was modified	`src/Pure/pure_thy.scala` (diff)
Changeset 68721:53ad5c01be3f by eberlm _eberlm@in.tum.de_: Small lemmas about analysis
The file was modified	`src/HOL/Analysis/Cauchy_Integral_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Analysis_Basics.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Transcendental.thy` (diff)
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/FPS_Convergence.thy` (diff)
The file was modified	`src/HOL/Analysis/Gamma_Function.thy` (diff)
The file was modified	`src/HOL/Analysis/Henstock_Kurzweil_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Path_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Set_Integral.thy` (diff)
The file was modified	`src/HOL/Archimedean_Field.thy` (diff)
The file was modified	`src/HOL/Complex.thy` (diff)
The file was modified	`src/HOL/Int.thy` (diff)
The file was modified	`src/HOL/Limits.thy` (diff)
The file was modified	`src/HOL/Real_Vector_Spaces.thy` (diff)
The file was modified	`src/HOL/Series.thy` (diff)
The file was modified	`src/HOL/Topological_Spaces.thy` (diff)
Changeset 68720:1e1818612124 by paulson: merged
Changeset 68719:8aedca31957d by paulson _lp15@cam.ac.uk_: de-applying
The file was modified	`src/HOL/List.thy` (diff)