[Isarmathlib-devel] (no subject)

[clefort]

Working thru the tutorials from http://www.cse.unsw.edu.au/%7Ekleing/ 
teaching/thprv-04/#dates

First Session.thy

term "x"
term "Suc x"
term "Succ x"
term "Suc x =  Succ y"

[1.] "x" is a free variable
[2.] "Suc x" assigns it to a natural number? Q.1
[3.] "Succ x" is also a free variable like "x" but
[4.' "Suc x = Succ y" assigns it to be a natural number? Q.2

Q.3 When doing  C-c-C-f : "theorem-find" when having more than 40  
found theorems, how do you scroll down to the other found theorems?

Lastly, Q.5 How can we download your theorems and start to use them  
in Isabelle/Isar sessions? Or is that part of the tutorial?

Thank you


Clinton R. LeFort



>