diff --git a/courseA/Alloy.html b/courseA/Alloy.html
index dc49db3..b886006 100644
--- a/courseA/Alloy.html
+++ b/courseA/Alloy.html
@@ -1,5 +1,5 @@
 <!DOCTYPE html>
-<html lang="ja" xmlns="http://www.w3.org/1999/html">
+<html lang="ja" xmlns="http://www.w3.org/1999/html" xmlns="http://www.w3.org/1999/html">
 <head>
     <meta charset="UTF-8">
     <style>
@@ -16,12 +16,12 @@
 <h1>【Alloy の概要説明】</h1>
 <p>
     本実験で用いる Alloy の概要について説明します．<br>
-    現時点で本ページの内容を完全に理解する必要はありません．課題に取り組む際に必要に応じて本ページを参照しながら進めるようにください．<br>
+    現時点では本ページの内容を完全に理解する必要はありません．課題に取り組む際に必要に応じて本ページを参照しながら進めるようにください．<br>
 </p>
 <hr/>
 <h2>形式的仕様記述言語とは？</h2>
 <p>
-    Alloy は代表的な形式的仕様記述言語の一つです．<br>
+    Alloy は代表的な<strong>形式的仕様記述言語</strong>の一つです．<br>
     形式的仕様記述言語とは，仕様を自然言語ではなく，論理式のような数学的に厳密に意味が定義された形式で記述する方法で，<br>
     <ul>
     <li>仕様を曖昧性なく厳密に記述することができる，</li>
@@ -41,7 +41,7 @@
 </p>
 <h3>Alloyによる仕様記述:</h3>
 <p>
-    Alloy では，集合と関係を中心に仕様を記述していきます．また，その記述は宣言的な形式で行われます．<br>
+    Alloy では，<strong>集合</strong>と<strong>関係</strong>を使って仕様を記述していきます．また，その記述は<strong>宣言的</strong>な形式で行われます．<br>
     宣言的記述の対義語は手続き的記述です．我々が通常用いるプログラミング言語では手続き的な記述が用いられています．手続き的な記述ではプログラムは基本的に一番上の行から順番に一行ずつ,
     記述された順に実行されていきます．<br>
     一方宣言的な記述では，記述の順序は関係ありません．すべての行が同時に成り立っていると考えます．連立方程式を考えてみると解りやすいと思います．
@@ -67,12 +67,12 @@
 <h3>Alloy による記述例:</h3>
 <p>
     以下の仕様記述では名前の集合を <code>Name</code>，アドレスの集合を <code>Addr</code>，アドレス帳の集合を <code>Book</code> で表しています．<br>
-    <c1>sig</c1> でこれらの集合を宣言しています．ここで集合はクラス，集合に属している各要素はインスタンスに相当すると考えてください．ただし，Alloy は宣言型の言語なので，インスタンスの状態を変えることができません．状態の変更前と変更後でインスタンスが異なると考えてください．<br>
+    <c1>sig</c1> でこれらの<strong>集合</strong>を宣言しています．ここで集合はクラス，集合に属している各要素はインスタンスに相当すると考えてください．ただし，Alloy は宣言型の言語なので，インスタンスの状態を変えることができません．状態の変更前と変更後でインスタンスが異なると考えてください．<br>
     <code>Book</code> は，2つのフィールド <code>owner</code> と <code>addr</code> を持っています．Alloy におけるフィールドは，インスタンスの内部構造を表すものではなく，基本的に2つの集合の要素間の関係を表しています．たとえば <code>Book</code> の <code>owner</code> フィールドは，<code>Book</code> の各要素に <code>Name</code> の要素を対応づける関係を表しています．フィールドの詳細な意味については後ほど説明します．<br>
 </p>
 <p>
     Alloy では，操作も関係で表されます．たとえば add 操作は，連絡先を登録する前の <code>Book</code> の状態と，登録した後の <code>Book</code> の状態の間の関係を表していると考えます．<br>
-    より具体的には <c1>pred</c1> を用いて，登録前の <code>Book</code> の状態 <code>b</code>，登録後の <code>Book</code> の状態 <code>b'</code>，登録する連絡先の名前 <code>n</code>，登録するアドレス <code>a</code> の間に成り立つ述語として定義されています．<br>
+    より具体的には <c1>pred</c1> を用いて，登録前の <code>Book</code> の状態 <code>b</code>，登録後の <code>Book</code> の状態 <code>b'</code>，登録する連絡先の名前 <code>n</code>，登録するアドレス <code>a</code> の間に成り立つ<strong>述語</strong>として定義されています．<br>
     述語の本体は 1つ以上の式によって構成されます．これらの式は変数間に成り立つ制約関係を表しているため記述順は関係ありません．たとえば，<code>b'.owner = b.owner</code> は，add 操作前の <code>Book</code> の <code>owner</code> と，add 操作後の <code>Book</code> の <code>owner</code> が同じであることを示しています．
     <code>b'.addr = b.addr + n -> a</code> は，add 操作前の <code>Book</code> の <code>addr</code> （<code>Book</code> の各インスタンスが持つ，名前とアドレスの対応表）に，名前 <code>n</code> とアドレス <code>a</code> の対応を付け足したものが，add 操作後の <code>Book</code> の <code>addr</code> になることを示しています．これらの式は順番を入れ替えても意味は変わりません．
 </p>
@@ -128,7 +128,7 @@
     Alloy では実行を可視化することができます．上の仕様記述内の <c1>run</c1> による実行を可視化したものが以下の図です．
 </p>
 <div class="img-center">
-    <img src="../img/Alloy/AlloySample.png" class ="before-image-size"><br>
+    <img src="../img/Alloy/AlloySimpleAddressBook.png" class ="before-image-size"><br>
 </div>
 <p>
     可視化では実行時に生成される1つのインスタンスが，1つの矩形で表されます．たとえば，図の上部に並んでいる4つの矩形は，<code>execute</code> 述語内で宣言されている4つの変数，<code>b0, b1, b2, b3</code>に対応しています．
