make latex happy

moved some theorems into HOL main corpus

misc tuning and modernization

more theorems for proof of concept for word type

official fact collection sign_simps

tuned proofs

avoid pseudo-collection to be used in generated proofs

moved comment to approproiate place

removed outcommented example which seems not to work as advertized

clear separation of types for bits (False / True) and Z2 (0 / 1)

generalized type classes for parity to cover word types also, which contain zero divisors

slightly more specialized name for type class

dropped weaker legacy alias

slightly more stringent ordering of theorems

removed relics of ASCII syntax for indexed big operators

dropped former legacy input abbreviations

using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax

prefer fixed simpset for proof procedure

tuned file system structure

avoid spammed sledgehammer proofs

added lemmas

proper URL;

merged;

Added tag Isabelle2019 for changeset 83774d669b51

handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury)

tuned;

tuned;

backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;

unused;

tuned messages;