src/HOL/Word/Examples/WordExamples.thy
changeset 29629 5111ce425e7a
parent 26086 3c243098b64a
child 29640 741f26190c96
equal deleted inserted replaced
29628:d9294387ab0e 29629:5111ce425e7a
     1 (* 
     1 (* 
     2   ID:     $Id$
       
     3   Author: Gerwin Klein, NICTA
     2   Author: Gerwin Klein, NICTA
     4 
     3 
     5   Examples demonstrating and testing various word operations.
     4   Examples demonstrating and testing various word operations.
     6 *)
     5 *)
     7 
     6 
     8 header "Examples of word operations"
     7 header "Examples of word operations"
     9 
     8 
    10 theory WordExamples imports WordMain
     9 theory WordExamples
       
    10 imports Word
    11 begin
    11 begin
    12 
    12 
    13 -- "modulus"
    13 -- "modulus"
    14 
    14 
    15 lemma "(27 :: 4 word) = -5" by simp
    15 lemma "(27 :: 4 word) = -5" by simp