*To*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>, Johannes Hölzl <hoelzl at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] operator on predicates and relations*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 3 Apr 2014 09:44:25 +0200*In-reply-to*: <533D0E37.8060001@aalto.fi>*References*: <CDD9A9D3-F081-422C-9364-DB0E3252A0C8@cam.ac.uk> <53299484.2030100@aalto.fi> <1395237305.2841.192.camel@lapnipkow5> <5329C4DD.1030706@aalto.fi> <532FF25A.9060408@inf.ethz.ch> <533D0E37.8060001@aalto.fi>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.4.0

Hi Viorel, On 03/04/14 09:31, Viorel Preoteasa wrote:

If you want to use more advanced definition facilities (definition/function/...), you should have a look at "context overloading ... begin" context blocks.Where can I find more information and examples about this mechanism?

overloading myop_A == "myop :: 'a A" begin definition myop_A :: "'a A" where "myop_A P = P" end Best, Andreas

**References**:**Re: [isabelle] operator on predicates and relations***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] operator on predicates and relations
- Next by Date: Re: [isabelle] I need an ML function to get the THY path and filename
- Previous by Thread: Re: [isabelle] operator on predicates and relations
- Next by Thread: Re: [isabelle] Code equation for term_of_integer contains illegal numeral expression
- Cl-isabelle-users April 2014 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