# HG changeset patch
# User haftmann
# Date 1360759132 -3600
# Node ID bee2678a3b61129481d5c734413b6eb633c4cb11
# Parent  ced7163f1fe4a96f2d89e48ad60938b1375b586e
tuned spelling

diff -r ced7163f1fe4 -r bee2678a3b61 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Wed Feb 13 12:06:21 2013 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy	Wed Feb 13 13:38:52 2013 +0100
@@ -216,7 +216,7 @@
   by (rule Heap_eqI) (simp add: change_def lookup_chain)
 
 
-text {* Non-interaction between imperative array and imperative references *}
+text {* Non-interaction between imperative arrays and imperative references *}
 
 lemma array_get_set [simp]:
   "Array.get (set r v h) = Array.get h"
@@ -263,7 +263,7 @@
 
 subsection {* Code generator setup *}
 
-text {* Intermediate operation avoids invariance problem in @{text Scala} (similiar to value restriction) *}
+text {* Intermediate operation avoids invariance problem in @{text Scala} (similar to value restriction) *}
 
 definition ref' where
   [code del]: "ref' = ref"