Changes

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

Changeset 71997:4a013c92a091 by haftmann: factored out auxiliary theory
The file was added	`src/HOL/Word/Bit_Lists.thy`
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/F.thy`
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/Round.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/Misc_Auxiliary.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/Word/Word_Examples.thy`
Changeset 71996:c7ac6d4f3914 by haftmann: prefer explicit proof
The file was modified	`src/HOL/Word/Word.thy`

Changeset 11182:a03e9b5d8dc9 by haftmann: factored out auxiliary theory
The file was modified	`thys/CAVA_Automata/Automata.thy`
The file was modified	`thys/CAVA_LTL_Modelchecker/SM/Impl/SM_Ample_Impl.thy`
The file was modified	`thys/CAVA_LTL_Modelchecker/SM/Refine/Rename_Cfg.thy`
The file was modified	`thys/IP_Addresses/NumberWang_IPv4.thy`
The file was modified	`thys/JinjaThreads/MM/JMM_Spec.thy`
The file was modified	`thys/Knuth_Morris_Pratt/KMP.thy`
The file was modified	`thys/LLL_Basis_Reduction/LLL_Impl.thy`
The file was modified	`thys/LLL_Basis_Reduction/Missing_Lemmas.thy`
The file was modified	`thys/Native_Word/Code_Symbolic_Bits_Int.thy`
The file was modified	`thys/Native_Word/Code_Target_Word_Base.thy`
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy`
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy`
The file was modified	`thys/VerifyThis2018/Challenge2.thy`
The file was modified	`thys/VerifyThis2018/Challenge3.thy`
The file was modified	`thys/Word_Lib/Bitwise.thy`
The file was modified	`thys/Word_Lib/Word_Lemmas.thy`