tuned spelling
authorhaftmann
Wed Feb 13 13:38:52 2013 +0100 (2013-02-13)
changeset 51090bee2678a3b61
parent 51089 ced7163f1fe4
child 51091 c007c6bf4a35
tuned spelling
src/HOL/Imperative_HOL/Ref.thy
     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"