SuccessChanges

Summary

  1. added lemma
  2. incorporated various material from the AFP into the distribution
  3. backed out experimental b67bab2b132c, which slipped in accidentally
  4. merged
  5. moved subset_image_inj into Hilbert_Choice
  6. Lindelöf spaces and supporting material
Changeset 70368:a7aba6db79a1 by nipkow:
added lemma
The file was modifiedsrc/HOL/Lattices_Big.thy (diff)
Changeset 70367:3ea80c950023 by haftmann:
incorporated various material from the AFP into the distribution
The file was modifiedsrc/HOL/List.thy (diff)
The file was modifiedsrc/HOL/Word/Bits_Bit.thy (diff)
The file was modifiedsrc/HOL/Word/Bits_Int.thy (diff)
The file was modifiedsrc/HOL/Word/Word.thy (diff)
Changeset 70366:ca9dfa7ee3bd by haftmann:
backed out experimental b67bab2b132c, which slipped in accidentally
The file was modifiedsrc/HOL/Eisbach/method_closure.ML (diff)
The file was modifiedsrc/Pure/Pure.thy (diff)
The file was modifiedsrc/Pure/Tools/named_theorems.ML (diff)
The file was modifiedsrc/Tools/atomize_elim.ML (diff)
Changeset 70365:93516cb6cd30 by nipkow:
merged
Changeset 70364:269dcea7426c by paulson <lp15@cam.ac.uk>:
moved subset_image_inj into Hilbert_Choice
The file was modifiedsrc/HOL/Hilbert_Choice.thy (diff)
The file was modifiedsrc/HOL/Library/Infinite_Set.thy (diff)
Changeset 70362:4900351361b0 by paulson <lp15@cam.ac.uk>:
Lindelöf spaces and supporting material
The file was addedsrc/HOL/Analysis/Lindelof_Spaces.thy
The file was modifiedsrc/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modifiedsrc/HOL/Analysis/Abstract_Topology_2.thy (diff)
The file was modifiedsrc/HOL/Analysis/Analysis.thy (diff)
The file was modifiedsrc/HOL/Analysis/Function_Topology.thy (diff)
The file was modifiedsrc/HOL/Analysis/Path_Connected.thy (diff)
The file was modifiedsrc/HOL/Analysis/Product_Topology.thy (diff)
The file was modifiedsrc/HOL/Analysis/T1_Spaces.thy (diff)
The file was modifiedsrc/HOL/Finite_Set.thy (diff)
The file was modifiedsrc/HOL/Homology/Simplices.thy (diff)
The file was modifiedsrc/HOL/Library/Countable_Set.thy (diff)
The file was modifiedsrc/HOL/Library/Infinite_Set.thy (diff)