1.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Wed Feb 13 12:06:21 2013 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Wed Feb 13 13:38:52 2013 +0100
     1.3 @@ -216,7 +216,7 @@
     1.4    by (rule Heap_eqI) (simp add: change_def lookup_chain)
     1.5  
     1.6  
     1.7 -text {* Non-interaction between imperative array and imperative references *}
     1.8 +text {* Non-interaction between imperative arrays and imperative references *}
     1.9  
    1.10  lemma array_get_set [simp]:
    1.11    "Array.get (set r v h) = Array.get h"
    1.12 @@ -263,7 +263,7 @@
    1.13  
    1.14  subsection {* Code generator setup *}
    1.15  
    1.16 -text {* Intermediate operation avoids invariance problem in @{text Scala} (similiar to value restriction) *}
    1.17 +text {* Intermediate operation avoids invariance problem in @{text Scala} (similar to value restriction) *}
    1.18  
    1.19  definition ref' where
    1.20    [code del]: "ref' = ref"