Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)
Summary
- build bit operations on word on library theory on bit operations
- more instances for uint types
- canonical bit shifts for word type, leaving duplicates as they are at the moment
- dropped yet another duplicate
- replaced mere alias by input abbreviation
- replaced mere alias by abbreviation
- replaced operation with weak abstraction by input abbreviation
- avoid compound operation
- replaced mere alias by input abbreviation
Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)
Summary
- more lemmas
- build bit operations on word on library theory on bit operations
- bit operations as distinctive library theory
- tweak for code generation
- pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
- more lemmas and less name space pollution
- canonical bit shifts for word type, leaving duplicates as they are at the moment
- essential instance about bit structure
- more transfer rules
- dropped yet another duplicate
- fundamental construction of word type following existing transfer rules
- replaced mere alias by input abbreviation
- replaced mere alias by abbreviation
- replaced operation with weak abstraction by input abbreviation
- avoid compound operation
- formal relationships between operations
- eliminated warnings
- replaced mere alias by input abbreviation
The file was modified | src/HOL/Parity.thy |
The file was modified | src/HOL/Word/Word.thy |
The file was modified | CONTRIBUTORS |
The file was modified | NEWS |
The file was modified | src/HOL/Library/Z2.thy |
The file was modified | src/HOL/Word/Bits.thy |
The file was modified | src/HOL/Word/Bits_Int.thy |
The file was modified | src/HOL/Word/Word.thy |
The file was modified | src/HOL/Word/Word_Bitwise.thy |
The file was removed | src/HOL/Word/Bits_Z2.thy |
The file was added | src/HOL/Library/Bit_Operations.thy |
The file was modified | CONTRIBUTORS |
The file was modified | NEWS |
The file was modified | src/HOL/Library/Library.thy |
The file was modified | src/HOL/ex/Word.thy |
The file was removed | src/HOL/ex/Bit_Operations.thy |
The file was modified | src/HOL/Word/Word.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 |
The file was modified | src/HOL/Word/Word_Examples.thy |
The file was modified | src/HOL/ex/Word.thy |
The file was modified | src/HOL/Library/Z2.thy |
The file was modified | src/HOL/Word/Word.thy |
The file was modified | src/HOL/Word/Word.thy |
The file was modified | src/HOL/Word/Word.thy |
The file was modified | src/HOL/Word/Word.thy |
The file was modified | NEWS |
The file was modified | src/HOL/Word/Bits_Int.thy |
The file was modified | src/HOL/Word/Word.thy |
The file was modified | src/HOL/Word/Word.thy |
The file was modified | NEWS |
The file was modified | src/HOL/Word/Bits_Int.thy |
The file was modified | src/HOL/Word/Word.thy |
The file was modified | NEWS |
The file was modified | src/HOL/Word/Bits_Int.thy |
The file was modified | src/HOL/Word/Word.thy |
The file was modified | src/HOL/Word/Word_Examples.thy |
The file was modified | NEWS |
The file was modified | src/HOL/Word/Bits_Int.thy |
The file was modified | src/HOL/Word/Word.thy |
The file was modified | NEWS |
The file was modified | src/HOL/Word/Bits_Int.thy |
The file was modified | src/HOL/Word/Word.thy |
The file was modified | src/HOL/Word/Bits_Int.thy |
The file was modified | src/HOL/Library/Cardinality.thy |
The file was modified | src/HOL/Library/Z2.thy |
The file was modified | src/HOL/Word/Bits_Int.thy |
The file was modified | src/HOL/Word/Misc_Typedef.thy |
The file was modified | src/HOL/Word/Word.thy |
The file was modified | NEWS |
The file was modified | src/HOL/Word/Bits_Int.thy |
The file was modified | src/HOL/Word/Word_Bitwise.thy |