src/HOL/Word/More_Word.thy
author paulson <lp15@cam.ac.uk>
Wed, 04 Sep 2019 16:34:45 +0100
changeset 70643 93a7a85de312
parent 70174 40fdd74b75f3
child 71985 a1cf296a7786
permissions -rw-r--r--
Removal of the redundant ancestor Continuous_Extension
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
70174
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Word/More_Word.thy
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents:
diff changeset
     2
*)
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents:
diff changeset
     3
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents:
diff changeset
     4
section \<open>Comprehensive Word Library\<close>
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents:
diff changeset
     5
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents:
diff changeset
     6
theory More_Word
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents:
diff changeset
     7
imports
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents:
diff changeset
     8
  Word
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents:
diff changeset
     9
  Word_Bitwise
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents:
diff changeset
    10
begin
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents:
diff changeset
    11
40fdd74b75f3 entry point for comprehensive word library
haftmann
parents:
diff changeset
    12
end