src/HOL/ex/IArray_Examples.thy
changeset 51094 84b03c49c223
parent 50138 ca989d793b34
child 51143 0a2371e7ced3
equal deleted inserted replaced
51093:9d7aa2bb097b 51094:84b03c49c223
     1 theory IArray_Examples
     1 theory IArray_Examples
     2 imports "~~/src/HOL/Library/IArray"
     2 imports "~~/src/HOL/Library/IArray" "~~/src/HOL/Library/Efficient_Nat"
     3 begin
     3 begin
     4 
     4 
     5 lemma "IArray [True,False] !! 1 = False"
     5 lemma "IArray [True,False] !! 1 = False"
     6 by eval
     6 by eval
     7 
     7 
    22 
    22 
    23 lemma "sum (IArray [1,2,3,4,5,6,7,8,9::int]) = 45"
    23 lemma "sum (IArray [1,2,3,4,5,6,7,8,9::int]) = 45"
    24 by eval
    24 by eval
    25 
    25 
    26 end
    26 end
       
    27