Changes

Summary

Changeset 71828:415c38ef38c0 by nipkow: added top-level functions and tuned
The file was modified	`src/HOL/Data_Structures/AVL_Bal_Set.thy` (diff)
Changeset 71827:5e315defb038 by paulson _lp15@cam.ac.uk_: the Uniq quantifier
The file was modified	`src/HOL/Analysis/Infinite_Products.thy` (diff)
The file was modified	`src/HOL/Analysis/Interval_Integral.thy` (diff)
The file was modified	`src/HOL/Deriv.thy` (diff)
The file was modified	`src/HOL/Fun.thy` (diff)
The file was modified	`src/HOL/HOL.thy` (diff)
The file was modified	`src/HOL/Hilbert_Choice.thy` (diff)
The file was modified	`src/HOL/Library/Infinite_Set.thy` (diff)
The file was modified	`src/HOL/Limits.thy` (diff)
The file was modified	`src/HOL/List.thy` (diff)
The file was modified	`src/HOL/Real_Vector_Spaces.thy` (diff)
The file was modified	`src/HOL/Relation.thy` (diff)
The file was modified	`src/HOL/Series.thy` (diff)
The file was modified	`src/HOL/Set.thy` (diff)
The file was modified	`src/HOL/Topological_Spaces.thy` (diff)
The file was modified	`src/HOL/Transfer.thy` (diff)
The file was modified	`src/HOL/Wellfounded.thy` (diff)