src/HOL/Word/WordMain.thy
author wenzelm
Tue, 10 Jun 2008 21:50:30 +0200
changeset 27137 d0070c32fdc1
parent 26560 d2fc9a18ee8a
permissions -rw-r--r--
fixed spelling (Where is WordExamples.thy anyway?);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     1
(* 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     2
  ID:     $Id$
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     3
  Author: Gerwin Klein, NICTA
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     4
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     5
  The main interface of the word library to other theories.
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     6
*)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     7
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
     8
header {* Main Word Library *}
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
     9
26560
haftmann
parents: 26086
diff changeset
    10
theory WordMain
haftmann
parents: 26086
diff changeset
    11
imports WordGenLib
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    12
begin
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    13
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 24350
diff changeset
    14
lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps]
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    15
lemmas word_no_0 [simp] = word_0_no [symmetric]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    16
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    17
declare word_0_bl [simp]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    18
declare bin_to_bl_def [simp]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    19
declare to_bl_0 [simp]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    20
declare of_bl_True [simp]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    21
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    22
text "Examples"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    23
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    24
types word32 = "32 word"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    25
types word8 = "8 word"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    26
types byte = word8
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    27
27137
d0070c32fdc1 fixed spelling (Where is WordExamples.thy anyway?);
wenzelm
parents: 26560
diff changeset
    28
text {* for more see WordExamples.thy *}
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    29
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    30
end