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.