diff --git a/README.md b/README.md
index 68848f7..47ebb56 100644
--- a/README.md
+++ b/README.md
@@ -8,6 +8,34 @@ A nuHFL(Z) (aka higher-order CHC) solver based on refinement types.
 =======
 Forked from https://github.com/moratorium08/hflmc2
 
+## Changes by Sato
+
+Support input files for annotations introduced by Yamada-san
+
+### How to use
+
+Use options `--annot <input.annot>` and `--target <CHECK_TARGET>` (See below for CHECK_TARGET). For example:
+
+```
+$ dune exec -- hflmc3 --no-disprove kmp.hfl --annot kmp.loop.annot --target toplevel
+```
+
+Here is an exmalpe of .annot file:
+```
+%TYPE
+
+LOOP:
+  (plen: int ->
+  (slen: int ->
+  ((i: int -> ((int -> *) -> *[(0 <= i /\ i < plen)])) ->
+  ((i: int -> ((v: int -> *[(0 <= v + 1 /\ v + 1 < plen)]) -> *[(0 <= i /\ i < plen)])) ->
+  ((i: int -> ((int -> *) -> *[(0 <= i /\ i < slen)])) ->
+  (s: int ->
+  (p: int ->
+  ((int -> *) ->
+  *[0<plen /\ 0<slen /\ 0<=p /\ 0<=s]))))))))
+```
+
 ## Changes by Yamada
 
 `lib/typing/rinfer.ml` を (dirty hack 的に) 改変して、`prop<tt>` 以外の推論ができるようにしています。