Skip to content
Success

Changes

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

Summary

  1. more operations;
  2. clarified signature;
  3. clarified signature;
  4. organize syntax for word operations in bundles
Changeset 74100:fb9c119e5b49 by wenzelm:
more operations;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74099:0bda15b1b937 by wenzelm:
clarified signature;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74098:5aaccec7c1a1 by wenzelm:
clarified signature;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74097:6d7be1227d02 by haftmann:
organize syntax for word operations in bundles
The file was modified NEWS
The file was modified src/HOL/Library/Bit_Operations.thy
The file was modified src/HOL/Library/Tools/smt_word.ML
The file was modified src/HOL/Library/Word.thy
The file was modified src/HOL/Library/Z2.thy
The file was modified src/HOL/SMT_Examples/SMT_Word_Examples.thy
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy
The file was modified src/HOL/SPARK/Manual/Reference.thy
The file was modified src/HOL/SPARK/SPARK.thy
The file was modified src/HOL/ex/Bit_Lists.thy

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. organize syntax for word operations in bundles
Changeset 11946:fc03e8f2954c by haftmann:
organize syntax for word operations in bundles
The file was modified thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy
The file was modified thys/Buchi_Complementation/Complementation_Final.thy
The file was modified thys/CAVA_LTL_Modelchecker/SM/Impl/SM_Ample_Impl.thy
The file was modified thys/CAVA_LTL_Modelchecker/SM/RefPoint/SM_Semantics.thy
The file was modified thys/CakeML/generated/CakeML/SemanticPrimitives.thy
The file was modified thys/CakeML/generated/Lem_word.thy
The file was modified thys/Collections/GenCF/Impl/Impl_Bit_Set.thy
The file was modified thys/Collections/GenCF/Impl/Impl_Uv_Set.thy
The file was modified thys/Complx/ex/SumArr.thy
The file was modified thys/IP_Addresses/IP_Address.thy
The file was modified thys/IP_Addresses/IPv4.thy
The file was modified thys/IP_Addresses/IPv6.thy
The file was modified thys/IP_Addresses/NumberWang_IPv6.thy
The file was modified thys/IP_Addresses/Prefix_Match.thy
The file was modified thys/Iptables_Semantics/Primitive_Matchers/IpAddresses.thy
The file was modified thys/JinjaThreads/Common/BinOp.thy
The file was modified thys/Native_Word/Bits_Integer.thy
The file was modified thys/Native_Word/Code_Symbolic_Bits_Int.thy
The file was modified thys/Native_Word/Code_Target_Bits_Int.thy
The file was modified thys/Native_Word/Code_Target_Word_Base.thy
The file was modified thys/Native_Word/Native_Word_Test.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/Native_Word/Word_Type_Copies.thy
The file was modified thys/PAC_Checker/PAC_Checker_Relation.thy
The file was modified thys/Refine_Imperative_HOL/benchmarks/Heapmap/isabelle/Heapmap_Bench.thy
The file was modified thys/SPARCv8/SparcModel_MMU/MMU.thy
The file was modified thys/SPARCv8/SparcModel_MMU/RegistersOps.thy
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Execution.thy
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Instruction.thy
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Properties.thy
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_State.thy
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Types.thy
The file was modified thys/Word_Lib/Aligned.thy
The file was modified thys/Word_Lib/Ancient_Numeral.thy
The file was modified thys/Word_Lib/Bits_Int.thy
The file was modified thys/Word_Lib/Examples.thy
The file was modified thys/Word_Lib/Guide.thy
The file was modified thys/Word_Lib/Legacy_Aliases.thy
The file was modified thys/Word_Lib/Many_More.thy
The file was modified thys/Word_Lib/More_Word.thy
The file was modified thys/Word_Lib/More_Word_Operations.thy
The file was modified thys/Word_Lib/Most_significant_bit.thy
The file was modified thys/Word_Lib/Reversed_Bit_Lists.thy
The file was modified thys/Word_Lib/Word_16.thy
The file was modified thys/Word_Lib/Word_32.thy
The file was modified thys/Word_Lib/Word_64.thy
The file was modified thys/Word_Lib/Word_8.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
The file was modified thys/Word_Lib/Word_Lib_Sumo.thy
The file was modified thys/Word_Lib/Word_Syntax.thy