Hi Johannes,
>> Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty
>> inf_top_right]
>> Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty
>> sup_bot_right]
>> INTER_eq_Inter_image ~> INF_def
>> UNION_eq_Union_image ~> SUP_def
>> INF_subset ~> INF_superset_mono [OF _ order_re
Hi Johannes,
> I tried to reduce the runtime requirement of HOL-Probability by removing
> some of the sublocale instantiations. As a lot of time is spend in
> locale interpretation inside proofs.
Is the same interpretation repeated over and over? In that case the
corresponding proposition can be
On Thu, 22 Sep 2011, Brian Huffman wrote:
Anyway, if we are decided that the legacy phase for renamed/generalized
theorems is not useful, then there is no point in preserving the "legacy
theorems" sections in the libraries, is there? We might as well go ahead
and start removing all of these ri
On Thu, 22 Sep 2011, Brian Huffman wrote:
I actually like Peter's idea of a "deprecated" flag better than my
Legacy.thy idea. We might implement it by adding a new "deprecated" flag
to each entry in the "naming" type implemented in
Pure/General/name_space.ML. Deprecated names would be treated
On 09/22/2011 09:00 PM, Lawrence Paulson wrote:
I think we are taking this idea too far.
The original suggestion was simply to move deprecated theorem
bindings into a separate file, where they could be loaded if
necessary to save people the trouble of having to edit their
theories.
But people
On Thu, Sep 22, 2011 at 11:34 AM, Alexander Krauss wrote:
> For mere renamings or simple generalizations, we should just go ahead,
> making sure that the conversion table is in the NEWS. Having an extra legacy
> phase here only creates extra work with no benefit for anyone. With a new
> release, p
I think we are taking this idea too far.
The original suggestion was simply to move deprecated theorem bindings into a
separate file, where they could be loaded if necessary to save people the
trouble of having to edit their theories. We could generalise the idea of a
little so that other delet
On 09/22/2011 05:00 PM, Brian Huffman wrote:
I actually like Peter's idea of a "deprecated" flag better than my
Legacy.thy idea. We might implement it by adding a new "deprecated"
flag to each entry in the "naming" type implemented in
Pure/General/name_space.ML. Deprecated names would be treated
On Thu, Sep 22, 2011 at 6:10 AM, Makarius wrote:
> On Thu, 22 Sep 2011, Lukas Bulwahn wrote:
>
>> On 09/22/2011 11:36 AM, Peter Lammich wrote:
>
> Perhaps we should start using a standardized process for phasing out
> legacy theorems, like moving them into a separate theory file
>
On Tue, 20 Sep 2011, Makarius wrote:
In the meantime I have investigated this a little bit. It seems that
HOL-Probability requires quite some memory even in minimalistic batch mode --
approx. 2GB on my 4GB machine. With Isabelle/jEdit one needs further 600 MB
for the editor process and the sa
In Java, there is a "deprecated" flag for such issues. Isabelle could
then issue
a warning whenever using a deprecated lemma --- like the "legacy"-warnings
it already issues when using some deprecated features (recdef, etc.)
You are assuming that you could flag theorems, and all tools know what
On Wed, 21 Sep 2011, Brian Huffman wrote:
On Tue, Sep 20, 2011 at 10:03 AM, Christian Urban wrote:
I was able to put together replacement theorems for a few of these lemmas:
Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right]
Sup_singleton ~> Sup_insert [where A="{}", u
On Thu, 22 Sep 2011, Lukas Bulwahn wrote:
On 09/22/2011 11:36 AM, Peter Lammich wrote:
Perhaps we should start using a standardized process for phasing out
legacy theorems, like moving them into a separate theory file
"Legacy.thy" that would not be imported by default, and would be
cleared out
On 09/22/2011 11:36 AM, Peter Lammich wrote:
Perhaps we should start using a standardized process for phasing out
legacy theorems, like moving them into a separate theory file
"Legacy.thy" that would not be imported by default, and would be
cleared out after each release. When upgrading Isabelle,
>> Perhaps we should start using a standardized process for phasing out
>> legacy theorems, like moving them into a separate theory file
>> "Legacy.thy" that would not be imported by default, and would be
>> cleared out after each release. When upgrading Isabelle, users could
>> import Legacy.thy
I think this is a good idea.
Larry
On 22 Sep 2011, at 03:08, Brian Huffman wrote:
> Perhaps we should start using a standardized process for phasing out
> legacy theorems, like moving them into a separate theory file
> "Legacy.thy" that would not be imported by default, and would be
> cleared out
16 matches
Mail list logo
