Changes

Summary

avoid name clash
lemma
tuned;
another example for lift_bnf for quotients

Changeset 73411:1f1366966296 by haftmann: avoid name clash
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Complete_Lattices.thy` (diff)
The file was modified	`src/HOL/Complete_Partial_Order.thy` (diff)
The file was modified	`src/HOL/Complex_Main.thy` (diff)
The file was modified	`src/HOL/Conditionally_Complete_Lattices.thy` (diff)
The file was modified	`src/HOL/Fields.thy` (diff)
The file was modified	`src/HOL/Groups.thy` (diff)
The file was modified	`src/HOL/Hilbert_Choice.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int3.thy` (diff)
The file was modified	`src/HOL/Lattices.thy` (diff)
The file was modified	`src/HOL/Lattices_Big.thy` (diff)
The file was modified	`src/HOL/Library/Complete_Partial_Order2.thy` (diff)
The file was modified	`src/HOL/Library/Countable_Complete_Lattices.thy` (diff)
The file was modified	`src/HOL/Library/DAList_Multiset.thy` (diff)
The file was modified	`src/HOL/Library/Lattice_Algebras.thy` (diff)
The file was modified	`src/HOL/Library/Multiset.thy` (diff)
The file was modified	`src/HOL/Library/Sublist.thy` (diff)
The file was modified	`src/HOL/Library/Subseq_Order.thy` (diff)
The file was modified	`src/HOL/List.thy` (diff)
The file was modified	`src/HOL/Nat.thy` (diff)
The file was modified	`src/HOL/Orderings.thy` (diff)
The file was modified	`src/HOL/Partial_Function.thy` (diff)
The file was modified	`src/HOL/Power.thy` (diff)
The file was modified	`src/HOL/Real_Vector_Spaces.thy` (diff)
The file was modified	`src/HOL/Set_Interval.thy` (diff)
The file was modified	`src/HOL/Topological_Spaces.thy` (diff)
The file was modified	`src/HOL/ex/Radix_Sort.thy` (diff)
Changeset 73410:7b59d2945e54 by haftmann: lemma
The file was modified	`src/HOL/Library/Permutations.thy` (diff)
Changeset 73409:fbd69f277699 by wenzelm: tuned;
The file was modified	`NEWS` (diff)
Changeset 73408:be11fe268b33 by traytel: another example for lift_bnf for quotients
The file was added	`src/HOL/Datatype_Examples/FAE_Sequence.thy`
The file was modified	`src/HOL/ROOT` (diff)