Changes

Summary

more theorems
Simplified, generalised version of Constructible due to E. Gunther, M. Pagano and P. Sánchez Terraf
tuned

Changeset 71418:bd9d27ccb3a3 by haftmann: more theorems
The file was modified	`src/HOL/Parity.thy` (diff)
The file was modified	`src/HOL/ex/Bit_Operations.thy` (diff)
The file was modified	`src/HOL/ex/Word.thy` (diff)
Changeset 71417:89d05db6dd1f by paulson _lp15@cam.ac.uk_: Simplified, generalised version of Constructible due to E. Gunther, M. Pagano and P. Sánchez Terraf
The file was modified	`src/ZF/Constructible/AC_in_L.thy` (diff)
The file was modified	`src/ZF/Constructible/DPow_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Datatype_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Formula.thy` (diff)
The file was modified	`src/ZF/Constructible/Internalize.thy` (diff)
The file was modified	`src/ZF/Constructible/L_axioms.thy` (diff)
The file was modified	`src/ZF/Constructible/Normal.thy` (diff)
The file was modified	`src/ZF/Constructible/Rank.thy` (diff)
The file was modified	`src/ZF/Constructible/Rank_Separation.thy` (diff)
The file was modified	`src/ZF/Constructible/Rec_Separation.thy` (diff)
The file was modified	`src/ZF/Constructible/Reflection.thy` (diff)
The file was modified	`src/ZF/Constructible/Relative.thy` (diff)
The file was modified	`src/ZF/Constructible/Satisfies_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Separation.thy` (diff)
The file was modified	`src/ZF/Constructible/WF_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Wellorderings.thy` (diff)
Changeset 71416:6a1c1d1ce6ae by nipkow: tuned
The file was modified	`src/HOL/Data_Structures/Interval_Tree.thy` (diff)