search

jrh13 / hol-light

The HOL Light theorem prover
Other
435 stars 78 forks source link

running example error when using tactics g #27

Open hoyeunglee opened 8 years ago

hoyeunglee commented 8 years ago

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 commented 7 years ago

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.