Re: [isabelle] Variables in locale assumptions



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 development that you think the "default" Isabelle style is appropriate for him? Or is it just the objectively "best" style?

Best
Benedikt




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.