[isabelle] Combining locales?



I want to have a locale combining two different lattices, and using
the infix syntax.  This goes back to help I got from this list several
months ago.  Here is a script that worked in Isabelle2011 (and I've
developed significant work in this locale) and fails in
Isabelle2011-1:

theory localeTypeUnif imports Main begin

locale labelAuth =
 label: lattice lblle lbllt lblinf lblsup
 +
 auth: lattice authle authlt authinf authsup
 for lblle::"'a \<Rightarrow> 'a \<Rightarrow> bool"    (infix
"\<sqsubseteq>" 50)
 and lbllt::"'a \<Rightarrow> 'a \<Rightarrow> bool"    (infix
"\<sqsubset>"  50)
 and lblinf::"'a \<Rightarrow> 'a \<Rightarrow> 'a"     (infixl
"\<sqinter>" 70)
 and lblsup::"'a \<Rightarrow> 'a \<Rightarrow> 'a"     (infixl
"\<squnion>" 65)
 and authle:: "'b \<Rightarrow> 'b \<Rightarrow> bool"  (infix
"\<sqsubseteq>" 50)
 and authlt:: "'b \<Rightarrow> 'b \<Rightarrow> bool"  (infix
"\<sqsubset>"  50)
 and authinf::"'b \<Rightarrow> 'b \<Rightarrow> 'b"    (infixl
"\<sqinter>" 70)
 and authsup::"'b \<Rightarrow> 'b \<Rightarrow> 'b"    (infixl
"\<squnion>" 65)

*** Type unification failed
***
*** Failed to meet type constraint:
***
*** Term:  op \<sqsubseteq> :: 'a \<Rightarrow> 'a \<Rightarrow> bool
*** Type:  'a \<Rightarrow> 'a \<Rightarrow> 'a
***
*** At command "locale" (line 3 of
"/home/rpollack/work/seas/crash/ubreeze/isabelle/experiments/localeTypeUnif.thy")

What is the problem?  Thanks for any help.

Randy





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.