running example error when using tactics g

[hoyeunglee]

http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf section 8.1 page 45

git clone https://github.com/jrh13/hol-light.git cd ./hol-light make

use "hol.ml";;

let hol_dir = "/home/martin/Downloads/hol-light";;

tutorial page 45

g '2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7';; e DISCH_TAC;;

g '2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7';;

^

Parse error: ';;' expected after [str_item](in [top_phrase])

[koenraat]

All HOL Light terms are contained within `` not ' '. The conversion from `` to '' sometimes happens when you're copying from e.g. a PDF.

`2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7` should work.