[isabelle-dev] HOL-Bali

[Stefan Berghofer]

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