On Tue, 11 Feb 2014, Clemens Ballarin wrote:
For the processing of locale expression, facts are not really required.
Having all information related to syntax should be sufficient. I cannot
tell, though, whether facts may contain syntax in disguise of certain
attributes.
In principle there
On 21 March, 2014 17:26 CET, Makarius makar...@sketis.net wrote:
On Tue, 11 Feb 2014, Clemens Ballarin wrote:
For the processing of locale expression, facts are not really required.
Having all information related to syntax should be sufficient. I cannot
tell, though, whether facts
This does not exhibit itself until the compromised locale context is
(re-)entered, and I think this is not desirable. My first
spontaneous thought is that strictness should not apply during the
initialisation of a locale context.
I wouldn't want to add special treatment for this. Currently
For the processing of locale expression, facts are not really required. Having
all information related to syntax should be sufficient. I cannot tell, though,
whether facts may contain syntax in disguise of certain attributes.
Clemens
On 10 February, 2014 16:14 CET, Makarius
On Fri, 10 Jan 2014, Clemens Ballarin wrote:
This does not exhibit itself until the compromised locale context is
(re-)entered, and I think this is not desirable. My first spontaneous
thought is that strictness should not apply during the initialisation
of a locale context.
I wouldn't want
On 28 December, 2013 19:53 CET, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
HOL-Complex now builds with strict naming policy for facts (again).
Thanks, that's cool.
I have stumbled over something which needs some consideration: with
strict naming policy, locales can
Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:
If you point we to particular
occurences, I am willing to polish them accordingly.
There are several versions of bounded_iff in the locales of that
theory (and lattice locales from imported theories). To find all
I recently tried to make HOL-Algebra compliant to this, but
unfortunately got stuck in HOL already, where Big_Operators didn't
comply either (but that's unlikely the only theory).
Yet another unintentional coincidence. If you point we to particular
occurences, I am willing to polish them
I recently tried to make HOL-Algebra compliant to this, but
unfortunately got stuck in HOL already, where Big_Operators didn't
comply either (but that's unlikely the only theory).
If we are serious about forbidding duplicate theorem names eventually
we probably need to start by introducing
On Thu, 11 Oct 2012, Johannes Hölzl wrote:
HOL-Probability (in Isabelle/bb5db3d1d6dd) and
Ordinary_Differential_Equations (in AFP/e9fa38f86b76) work now with this
patch.
A surprising change is found in Markov_Models:
We get an error when an assumption has the same name as a fact in the
HOL-Probability (in Isabelle/bb5db3d1d6dd) and
Ordinary_Differential_Equations (in AFP/e9fa38f86b76) work now with this
patch.
A surprising change is found in Markov_Models:
We get an error when an assumption has the same name as a fact in the
locale:
locale loc
begin
lemma X:
Am Sonntag, den 07.10.2012, 18:06 +0200 schrieb Lars Noschinski:
On 07.10.2012 09:37, Florian Haftmann wrote:
Hi all,
currently, theorem names in locales can be shadowed (given that
declarations are in different theories, otherwise the foundation level
would reject the declaration since
On 07.10.2012 09:37, Florian Haftmann wrote:
Hi all,
currently, theorem names in locales can be shadowed (given that
declarations are in different theories, otherwise the foundation level
would reject the declaration since the two foundation theorems would
have the same name).
After some
13 matches
Mail list logo
