Skip to content
[Jenkins]Jenkins
log in
Success

Changes

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

Summary

  1. more distinctive theory structure
  2. clarified notation
Changeset 10374:91971ca6ad5e by haftmann:
more distinctive theory structure
The file was addedthys/Native_Word/Code_Symbolic_Bits_Int.thy
The file was addedthys/Native_Word/Code_Target_Word_Base.thy
The file was modified thys/CAVA_LTL_Modelchecker/SM/RefPoint/SM_State.thy
The file was modified thys/JinjaThreads/Execute/Java2Jinja.thy
The file was modified thys/Native_Word/Bits_Integer.thy
The file was modified thys/Native_Word/Code_Target_Bits_Int.thy
The file was modified thys/Native_Word/More_Bits_Int.thy
The file was modified thys/Native_Word/Native_Word_Imperative_HOL.thy
The file was modified thys/Native_Word/ROOT
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 removedthys/Native_Word/Word_Misc.thy
Changeset 10373:3eabfd50bfba by haftmann:
clarified notation
The file was modified thys/CAVA_LTL_Modelchecker/SM/RefPoint/SM_State.thy
The file was modified thys/Collections/GenCF/Impl/Impl_Uv_Set.thy
The file was modified thys/Containers/ITP-2013/Benchmark_Set.thy
The file was modified thys/IP_Addresses/CIDR_Split.thy
The file was modified thys/IP_Addresses/IP_Address.thy
The file was modified thys/IP_Addresses/IP_Address_toString.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/Lib_Word_toString.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/Kleene_Algebra/Matrix.thy
The file was modified thys/LOFT/LinuxRouter_OpenFlow_Translation.thy
The file was modified thys/Native_Word/Uint.thy
The file was modified thys/Native_Word/Word_Misc.thy
The file was modified thys/Refine_Monadic/examples/WordRefine.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_Types.thy
The file was modified thys/Word_Lib/Aligned.thy
The file was modified thys/Word_Lib/Norm_Words.thy
The file was modified thys/Word_Lib/Signed_Words.thy
The file was modified thys/Word_Lib/Word_Enum.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
The file was modified thys/Word_Lib/Word_Lib.thy
The file was modified thys/Word_Lib/Word_Setup_32.thy
The file was modified thys/Word_Lib/Word_Setup_64.thy

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

Summary

  1. clarified notation
Changeset 70185:ac1706cdde25 by haftmann:
clarified notation
The file was modified src/HOL/Library/Saturated.thy
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
The file was modified src/HOL/SPARK/SPARK.thy
The file was modified src/HOL/Word/Word.thy
The file was modified src/HOL/Word/Word_Bitwise.thy