[isabelle] Problems using lattices



I'm having problems using lattices. I know that any powerset is a lattice, and therefore I ought to be able to use lattice operations like \<sqinter>. I can certainly use \<inter> (the "cap" operation) on elements of a powerset; thus I can write lemma rule9: "((C::int set) \<inter> D) = (D \<inter> C)" by (rule Int_commute) where \<inter> is replaced by cap. That works. But when I try the same thing with lattice operations, like this: lemma rule11: "((C::int set) \<sqinter> D) = (D \<sqinter> C)" by (rule INF_commute) where \<sqinter> is replaced by the "square cap" operation, I get the message "Inner lexical error -- Failed to parse prop". What else do I need in order to get this to work? Thanks! -WDMaurer
--
Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875




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