Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

Summary

  1. consolidated map2 clones
  2. separate type class for bit comprehension
  3. no need to maintain two separate type classes
  4. dropped obsolete import
  5. prefer map2 from Main HOL
Changeset 10379:6bd749578d6d by haftmann:
consolidated map2 clones
The file was modified thys/Jinja/DFA/Listn.thy
The file was modified thys/JinjaThreads/DFA/Listn.thy
The file was modified thys/List-Infinite/ListInf/List2.thy
The file was modified thys/Native_Word/Uint.thy
The file was modified thys/Native_Word/Uint16.thy
The file was modified thys/Native_Word/Uint32.thy
The file was modified thys/Native_Word/Uint64.thy
The file was modified thys/Native_Word/Uint8.thy
The file was modified thys/Sort_Encodings/G.thy
The file was modified thys/Sort_Encodings/Preliminaries.thy
The file was modified thys/Word_Lib/Aligned.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
Changeset 10378:ee820faeda58 by haftmann:
separate type class for bit comprehension
The file was modified thys/Native_Word/Bits_Integer.thy
The file was modified thys/Native_Word/Code_Target_Word_Base.thy
The file was modified thys/Native_Word/More_Bits_Int.thy
Changeset 10377:07087cf6c794 by haftmann:
no need to maintain two separate type classes
The file was modified thys/CAVA_Automata/CAVA_Base/CAVA_Base.thy
The file was modified thys/Collections/GenCF/Impl/Impl_Uv_Set.thy
The file was modified thys/Native_Word/Bits_Integer.thy
The file was modified thys/Native_Word/Uint.thy
The file was modified thys/Native_Word/Uint16.thy
The file was modified thys/Native_Word/Uint32.thy
The file was modified thys/Native_Word/Uint64.thy
The file was modified thys/Native_Word/Uint8.thy
Changeset 10376:8ffbee5ea590 by haftmann:
dropped obsolete import
The file was modified thys/Native_Word/More_Bits_Int.thy
Changeset 10375:9819993ba38c by haftmann:
prefer map2 from Main HOL
The file was modified thys/Affine_Arithmetic/Executable_Euclidean_Space.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Abstract_Rigorous_Numerics.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics_Aform.thy
The file was modified thys/Ordinary_Differential_Equations/Refinement/Refine_Vector_List.thy
The file was modified thys/Taylor_Models/Polynomial_Expression_Additional.thy
The file was modified thys/Taylor_Models/Taylor_Models.thy

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. consolidated map2 clones
  2. separate type class for bit comprehension
  3. no need to maintain two separate type classes
  4. clarified structure of theories
Changeset 70193:49a65e3f04c9 by haftmann:
consolidated map2 clones
The file was modified src/HOL/Word/Bits_Int.thy
The file was modified src/HOL/Word/Misc_Auxiliary.thy
The file was modified src/HOL/Word/Word.thy
The file was modified src/HOL/Word/Word_Bitwise.thy
Changeset 70192:b4bf82ed0ad5 by haftmann:
separate type class for bit comprehension
The file was addedsrc/HOL/Word/Bit_Comprehension.thy
The file was modified src/HOL/Word/Bits.thy
The file was modified src/HOL/Word/Bits_Int.thy
The file was modified src/HOL/Word/Word.thy
Changeset 70191:bdc835d934b7 by haftmann:
no need to maintain two separate type classes
The file was modified src/HOL/Word/Bits.thy
The file was modified src/HOL/Word/Bits_Bit.thy
The file was modified src/HOL/Word/Bits_Int.thy
The file was modified src/HOL/Word/Word.thy
Changeset 70190:ff9efdc84289 by haftmann:
clarified structure of theories
The file was addedsrc/HOL/Word/Misc_Auxiliary.thy
The file was modified src/HOL/Word/Bits.thy
The file was modified src/HOL/Word/Bits_Int.thy
The file was modified src/HOL/Word/Misc_Arithmetic.thy
The file was modified src/HOL/Word/Word.thy
The file was modified src/HOL/Word/Word_Bitwise.thy
The file was removedsrc/HOL/Word/Bit_Representation.thy
The file was removedsrc/HOL/Word/Bool_List_Representation.thy