Lawrence Paulson wrote: > I am trying to test some minor changes, but I can't get HOL to run. The > crazy thing is that I cannot see anything wrong with the syntax of that > lemma: > > lemma triangle_lemma: > "\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> > \<Longrightarrow> b=c; (a,x)\<in>r*; (a,y)\<in>r*\<rbrakk> > \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
Hi Larry, it seems that the \<^sup> in r\<^sup>* has disappeared. Maybe some Emacs oddity? Greetings, Stefan -- Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de Institut fuer Informatik Phone: +49 89 289 17328 Technische Universitaet Muenchen Fax: +49 89 289 17307 Boltzmannstr. 3 Room: 01.11.059 85748 Garching, GERMANY http://www.in.tum.de/~berghofe
