*To*: bnord <bnord01 at gmail.com>*Subject*: Re: [isabelle] Variables in locale assumptions*From*: Makarius <makarius at sketis.net>*Date*: Mon, 24 Feb 2014 13:47:54 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5307909E.2020300@gmail.com>*References*: <FC4BBC48012AB34DAF828891BA6076320A6BED6F@MBX21.d.ethz.ch>, <D85BDDB5-D8F4-4F4C-A578-35FD64B33584@cantab.net> <FC4BBC48012AB34DAF828891BA6076320A6BEE7C@MBX21.d.ethz.ch> <alpine.LNX.2.00.1402211828050.46463@lxbroy10.informatik.tu-muenchen.de> <5307909E.2020300@gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 21 Feb 2014, bnord wrote:

Am 21.02.2014 18:33, schrieb Makarius:Note that "Test" is a bad name for a locale: lower-case is normally used. Likewise, theory names are usually capitalized words (in singular), separated by underscore. (You did not show that in the example, but I guess > 50% that you've had a lowercase test.thy here, or was it just Scratch.thy?)

Do you know anything about the intended audience for his developmentthat you think the "default" Isabelle style is appropriate for him? Oris it just the objectively "best" style?

Makarius

**References**:**[isabelle] Variables in locale assumptions***From:*Van Staden Stephan

**Re: [isabelle] Variables in locale assumptions***From:*John Wickerson

**Re: [isabelle] Variables in locale assumptions***From:*Van Staden Stephan

**Re: [isabelle] Variables in locale assumptions***From:*Makarius

**Re: [isabelle] Variables in locale assumptions***From:*bnord

- Previous by Date: Re: [isabelle] Variables in locale assumptions
- Next by Date: Re: [isabelle] Variables in locale assumptions
- Previous by Thread: Re: [isabelle] Variables in locale assumptions
- Next by Thread: Re: [isabelle] Variables in locale assumptions
- Cl-isabelle-users February 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