Session Word_Lib

Theories

• Enumeration
• Even_More_List
• HOL-Library.Phantom_Type
• HOL-Library.Cardinality
• HOL-Library.Numeral_Type
• HOL-Library.Type_Length
• HOL-Library.Word
  • File ‹Tools/word_lib.ML›
  • File ‹Tools/smt_word.ML›
• Legacy_Aliases
• More_Arithmetic
• More_Divides
• More_Misc
• HOL-Library.Sublist
• More_Sublist
• More_Bit_Ring
• More_Word
• Strict_part_mono
• Bit_Shifts_Infix_Syntax
• Most_significant_bit
• Least_significant_bit
• Generic_set_bit
• Bit_Comprehension
• Bits_Int
• Aligned
• Next_and_Prev
• HOL-Library.Signed_Division
• Signed_Division_Word
• Many_More
• Singleton_Bit_Shifts
• Typedef_Morphisms
• Reversed_Bit_Lists
• Bitwise
• Bit_Comprehension_Int
• Signed_Words
• Bitwise_Signed
• Enumeration_Word
• Hex_Words
• Norm_Words
• Rsplit
• Syntax_Bundles
• Sgn_Abs
• Type_Syntax
• HOL-Eisbach.Eisbach
  • File ‹parse_tools.ML›
  • File ‹method_closure.ML›
  • File ‹eisbach_rule_insts.ML›
  • File ‹match_method.ML›
• HOL-Eisbach.Eisbach_Tools
• Word_EqI
• Boolean_Inequalities
• Word_Lemmas
• Word_8
• Word_16
• Word_Syntax
• Word_Names
• More_Word_Operations
• Word_32
• Word_Lib_Sumo
• Machine_Word_32_Basics
• Machine_Word_32
• Word_64
• Machine_Word_64_Basics
• Machine_Word_64
• Guide
• Examples