# Re: [isabelle] locale

On 07/03/17 19:44, Michel via Cl-isabelle-users wrote:
> I am doing the proofs of a theory De_Morgan.thy (sent by Makarius) which
> is a sequence of lemmas whose I have to prove. Some lemmas are
> intuitionistic, others require the axiom classical. This axiom is
> defined as in the isar-ref p44, Â2.3.4 by
>
> locale classical =
> assumes classical :"(ÂC â C) â C" begin ...lemmas using classical end
>
> But when, in the same theory, I want to write again "locale classical",
> I have a message "Duplicate definition of De_Morgan.classical".
Such a locale is defined once and re-entered multiple times, e.g. via
context classical
begin
lemma ...
end
Or shorter:
lemma (in classical) ...
In some of my examples and exercises, I have used "notepad" with "have"
statements instead of topmost lemma. In a notepad, you cannot operate on
locales as above.
Makarius

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