[isabelle-dev] HOL-Bali

[Lawrence Paulson]

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*"
proof -

There are no invisible characters either. Does anybody have an idea?

Larry

Running HOL-Bali ...
HOL-Bali FAILED
(see also /Users/lp15/.isabelle/heaps//polyml-5.2.1_x86-darwin/log/HOL- 
Bali)

*** Theory loader: failed to load "Value" (unresolved "Type")
*** Theory loader: failed to load "Type" (unresolved "Name")
*** Theory loader: failed to load "Name" (unresolved "Basis")
*** Inner syntax error (line 66 of "/Users/lp15/isabelle/Repos/src/HOL/ 
Bali/Basis.thy") at ";
***   ( a , y ) \<in> r * \<rbrakk> \<Longrightarrow> ( x , y ) \<in>  
r * \<or>
***   ( y , x ) \<in> r *"
*** Failed to parse proposition (line 66 of "/Users/lp15/isabelle/ 
Repos/src/HOL/Bali/Basis.thy")
*** At command "lemma" (line 65 of "/Users/lp15/isabelle/Repos/src/HOL/ 
Bali/Basis.thy").
Exception- TOPLEVEL_ERROR raised
*** ML error

make: *** [/Users/lp15/.isabelle/heaps//polyml-5.2.1_x86-darwin/log/ 
HOL-Bali.gz] Error 1
~/isabelle/Repos/src/HOL: