*To*: David Streader <dstr at cs.waikato.ac.nz>*Subject*: Re: [isabelle] Can I assume an interpretation*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Mon, 7 Apr 2008 16:32:58 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <47F98BEB.1020802@cs.waikato.ac.nz>*References*: <47F98BEB.1020802@cs.waikato.ac.nz>

Hi David,

lemma transref: "a \<sqsubseteq> b \<longrightarrow> b\<sqsubseteq> c \<longrightarrow> a \<sqsubseteq> c"See attached file for very short theory containing details.But I am unable to proceed with this lemma. To the best of myunderstanding the assumption "a \<sqsubseteq> b " includes anassumption that "a c" are an interpretation of the local bop.

Clemens

**References**:**[isabelle] Can I assume an interpretation***From:*David Streader

- Previous by Date: Re: [isabelle] metis behaviour
- Next by Date: Re: [isabelle] Can I assume an interpretation
- Previous by Thread: [isabelle] Can I assume an interpretation
- Next by Thread: Re: [isabelle] Can I assume an interpretation
- Cl-isabelle-users April 2008 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