Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. moved subset_image_inj into Hilbert_Choice
  2. Lindelöf spaces and supporting material
  3. hierarchically inclusive named theorem collections
  4. removed unused fact collections
  5. eliminated type class
  6. entry point for comprehensive word library
  7. tuned theory names
  8. integrated Bit_Comparison into Word corpus
  9. tuned
  10. prefer one theory for misc material
  11. moved instance to appropriate place
Changeset 70179:269dcea7426c by paulson _lp15@cam.ac.uk_:
moved subset_image_inj into Hilbert_Choice
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Library/Infinite_Set.thy (diff)
Changeset 70178: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 modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Topology_2.thy (diff)
The file was modified src/HOL/Analysis/Analysis.thy (diff)
The file was modified src/HOL/Analysis/Function_Topology.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Product_Topology.thy (diff)
The file was modified src/HOL/Analysis/T1_Spaces.thy (diff)
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Homology/Simplices.thy (diff)
The file was modified src/HOL/Library/Countable_Set.thy (diff)
The file was modified src/HOL/Library/Infinite_Set.thy (diff)
Changeset 70177:b67bab2b132c by haftmann:
hierarchically inclusive named theorem collections
The file was modified src/HOL/Eisbach/method_closure.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/Tools/named_theorems.ML (diff)
The file was modified src/Tools/atomize_elim.ML (diff)
Changeset 70176:330382e284a4 by haftmann:
removed unused fact collections
The file was modified src/HOL/Rings.thy (diff)
Changeset 70175:85fb1a585f52 by haftmann:
eliminated type class
The file was modified NEWS (diff)
The file was modified src/HOL/Word/Bits.thy (diff)
The file was modified src/HOL/Word/Bits_Int.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)
Changeset 70174:40fdd74b75f3 by haftmann:
entry point for comprehensive word library
The file was addedsrc/HOL/Word/More_Word.thy
The file was modified NEWS (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 70173:c2786fe88064 by haftmann:
tuned theory names
The file was addedsrc/HOL/Word/Word_Bitwise.thy
The file was addedsrc/HOL/Word/Word_Examples.thy
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/Word/Word.thy (diff)
The file was removedsrc/HOL/Word/WordBitwise.thy
The file was removedsrc/HOL/Word/WordExamples.thy
Changeset 70172:c247bf924d25 by haftmann:
integrated Bit_Comparison into Word corpus
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/SPARK/SPARK_Setup.thy (diff)
The file was modified src/HOL/Word/Bits_Int.thy (diff)
The file was removedsrc/HOL/Word/Bit_Comparison.thy
Changeset 70171:3173d7878274 by haftmann:
tuned
The file was modified src/HOL/ex/Word_Type.thy (diff)
Changeset 70170:56727602d0a5 by haftmann:
prefer one theory for misc material
The file was addedsrc/HOL/Word/Misc_Arithmetic.thy
The file was modified src/HOL/Word/Bit_Representation.thy (diff)
The file was modified src/HOL/Word/Bits_Int.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)
The file was removedsrc/HOL/Word/Misc_Numeric.thy
The file was removedsrc/HOL/Word/Word_Miscellaneous.thy
Changeset 70169:8bb835f10a39 by haftmann:
moved instance to appropriate place
The file was modified src/HOL/Word/Bit_Representation.thy (diff)
The file was modified src/HOL/Word/Bits_Int.thy (diff)
The file was modified src/HOL/Word/Bool_List_Representation.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)
The file was modified src/HOL/Word/Word_Miscellaneous.thy (diff)