src/HOL/Word/More_Word.thy
author haftmann
Wed, 01 Jul 2020 17:32:11 +0000
changeset 71986 76193dd4aec8
parent 71985 a1cf296a7786
child 71997 4a013c92a091
permissions -rw-r--r--
factored out ancient numeral representation
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
71985
a1cf296a7786 moved to Word_Lib
haftmann
parents: 70174
diff changeset
     4
section \<open>Ancient comprehensive Word Library\<close>
70174
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
71986
76193dd4aec8 factored out ancient numeral representation
haftmann
parents: 71985
diff changeset
     9
  Ancient_Numeral
70174
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