*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] naming conventions (was "Want to use Rep_Integ or lifting after [quot_del] in Int.thy")*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Fri, 24 May 2013 15:45:37 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1305241813540.4879@macbroy21.informatik.tu-muenchen.de>*References*: <519AE86B.2030208@gmx.com> <3E3AEE15-2181-46D1-A676-85F7EC6FE1A4@cam.ac.uk> <519C3A46.3080901@gmx.com> <1369205906.2505.14.camel@macbroy12.informatik.tu-muenchen.de> <519CC513.8080202@gmx.com> <151E5274-D2DE-4AAB-ABC0-25BCE2244C0C@cam.ac.uk> <519CD00A.6070202@gmx.com> <519D78F2.1010002@gmail.com> <519D8EC6.6010907@gmx.com> <alpine.LNX.2.00.1305231325410.5918@macbroy21.informatik.tu-muenchen.de> <519F7571.304@gmx.com> <alpine.LNX.2.00.1305241813540.4879@macbroy21.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 5/24/2013 11:18 AM, Makarius wrote:

In the worst case, something like "user of Isabelle" will always work. Makarius

"What do you do?" "I do Oracle."

"What do you do?" "I write HOL source."

Instead of, "What do you do?" "I'm a programmer."

Regards, GB

**References**:**[isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy***From:*Gottfried Barrow

**Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy***From:*Lawrence Paulson

**Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy***From:*Gottfried Barrow

**Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy***From:*Johannes Hölzl

**Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy***From:*Gottfried Barrow

**Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy***From:*Lawrence Paulson

**Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy***From:*Gottfried Barrow

**[isabelle] naming conventions (was "Want to use Rep_Integ or lifting after [quot_del] in Int.thy")***From:*Christian Sternagel

**Re: [isabelle] naming conventions (was "Want to use Rep_Integ or lifting after [quot_del] in Int.thy")***From:*Gottfried Barrow

**Re: [isabelle] naming conventions (was "Want to use Rep_Integ or lifting after [quot_del] in Int.thy")***From:*Makarius

**Re: [isabelle] naming conventions (was "Want to use Rep_Integ or lifting after [quot_del] in Int.thy")***From:*Gottfried Barrow

*From:*Makarius

- Previous by Date: Re: [isabelle] naming conventions (was "Want to use Rep_Integ or lifting after [quot_del] in Int.thy")
- Next by Date: Re: [isabelle] record in a locale?
- Previous by Thread: Re: [isabelle] naming conventions (was "Want to use Rep_Integ or lifting after [quot_del] in Int.thy")
- Next by Thread: Re: [isabelle] naming conventions (was "Want to use Rep_Integ or lifting after [quot_del] in Int.thy")
- Cl-isabelle-users May 2013 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