*To*: Randy Pollack <rpollack at inf.ed.ac.uk>*Subject*: Re: [isabelle] lattices, typeclasses, notations?*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Fri, 27 May 2011 22:54:42 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <BANLkTim4NOUps-hmB2UK_bd-XMJp=FFqnQ@mail.gmail.com>*References*: <BANLkTim4NOUps-hmB2UK_bd-XMJp=FFqnQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.16) Gecko/20101227 Icedove/3.0.11

Hi Randy, [...]

However as a typeclass instantiation I get stuck: instantiation policy::partial_order

begin definition "leq = policyOrder" instance proof (intro_classes) The first goal is \<And>x. x \<sqsubseteq> x So I try fix x::policy show "x \<sqsubseteq> x" Already this is not accepted. Perhaps there is an ambiguity between the \<sqsubseteq> of policyOrder and the \<sqsubseteq> of the partial_order class (in spite of the explicit annotation (x::policy"). So I try fix x::policy show "leq x x" using policyOrderRfl . Here the "show" is accepted, but the last step "." still fails. What is my problem? Thanks for any info.

Hope this helps, Alex

**Follow-Ups**:**Re: [isabelle] lattices, typeclasses, notations?***From:*Randy Pollack

**References**:**[isabelle] lattices, typeclasses, notations?***From:*Randy Pollack

- Previous by Date: [isabelle] lattices, typeclasses, notations?
- Next by Date: Re: [isabelle] Storing data in a locale
- Previous by Thread: [isabelle] lattices, typeclasses, notations?
- Next by Thread: Re: [isabelle] lattices, typeclasses, notations?
- Cl-isabelle-users May 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list