Thanks! That solved it. (I really should have thought of the backquotes
myself, though.)
Felix
2012/4/30 Freek Wiedijk <[email protected]>
> Hi Felix,
>
> >4) I start gvim and load a file with the following content:
> >
> >let ARITHMETIC_SUM = thm ';
> > !n. nsum(1..n) (\i. i) = (n*(n+1)) DIV 2
> > proof
> > qed by #INDUCT_TAC;
> >';;
>
> The quotes should be backquotes. With this I think miz3
> will try to execute this as ocaml source (it does not match
> the pattern of a miz3 lemma). You can check this theory by
> pasting the same text in the ocaml session to see whether
> you get the same ocmal error.
>
> Anyway, it should be backquotes. Proofs are `; ... `
> instead of '; ... '
>
> Freek
>
--
http://www.felixbreuer.net
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
