Changes

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

Summary

integrated generic conversions into word corpse
more lemmas

Changeset 72262:a282abb07642 by haftmann: integrated generic conversions into word corpse
The file was modified	`src/HOL/Divides.thy`
The file was modified	`src/HOL/Library/Bit_Operations.thy`
The file was modified	`src/HOL/Parity.thy`
The file was modified	`src/HOL/ROOT`
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/F.thy`
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy`
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/Round.thy`
The file was modified	`src/HOL/Word/More_Word.thy`
The file was modified	`src/HOL/Word/Word.thy`
The file was modified	`src/HOL/ex/Bit_Lists.thy`
The file was removed	`src/HOL/Word/Conversions.thy`
Changeset 72261:5193570b739a by haftmann: more lemmas
The file was modified	`src/HOL/Divides.thy`
The file was modified	`src/HOL/Library/Bit_Operations.thy`
The file was modified	`src/HOL/Parity.thy`
The file was modified	`src/HOL/Word/Bits_Int.thy`
The file was modified	`src/HOL/Word/Conversions.thy`
The file was modified	`src/HOL/Word/Word.thy`

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

Summary

integrated generic conversions into word corpse
adjusted to changes in distribution

Changeset 11280:58bc7e81bc7f by haftmann: integrated generic conversions into word corpse
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy`
The file was modified	`thys/CAVA_LTL_Modelchecker/SM/RefPoint/SM_State.thy`
The file was modified	`thys/IEEE_Floating_Point/Conversion_IEEE_Float.thy`
The file was modified	`thys/IP_Addresses/CIDR_Split.thy`
The file was modified	`thys/IP_Addresses/IP_Address_Parser.thy`
The file was modified	`thys/IP_Addresses/IPv4.thy`
The file was modified	`thys/IP_Addresses/IPv6.thy`
The file was modified	`thys/Interval_Arithmetic_Word32/Interval_Word32.thy`
The file was modified	`thys/Iptables_Semantics/Common/Word_Upto.thy`
The file was modified	`thys/JinjaThreads/Compiler/Correctness1.thy`
The file was modified	`thys/JinjaThreads/Compiler/J1.thy`
The file was modified	`thys/JinjaThreads/J/SmallStep.thy`
The file was modified	`thys/Native_Word/Code_Target_Word_Base.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/SPARCv8/SparcModel_MMU/Sparc_Properties.thy`
The file was modified	`thys/Word_Lib/Aligned.thy`
The file was modified	`thys/Word_Lib/Word_Lemmas.thy`
The file was modified	`thys/Word_Lib/Word_Lemmas_32.thy`
The file was modified	`thys/Word_Lib/Word_Lemmas_64.thy`
The file was modified	`thys/Word_Lib/Word_Lib.thy`
The file was modified	`thys/Word_Lib/Word_Next.thy`
Changeset 11279:85d5b6c0bb92 by haftmann: adjusted to changes in distribution
The file was modified	`thys/Native_Word/Code_Target_Word_Base.thy`