On 04/16/2012 09:13 AM, Christian Sternagel wrote:
Hi all,
On 04/03/2012 02:51 AM, Florian Haftmann wrote:
well, I suggest to augment the existing theory with lemmas transferred
from relpow to relpowp to emphasize that both worlds exists and that
lemmas can be found easier by find_theorems. The typical pattern is
lemma foo_relpow: ...
<proof>
lemma foo_relpowp: ...
by (fact foo_relpow [to_pred])
I did this in the meantime (tested with "isabelle makeall all"). This
time as a patch (in order to avoid cluttering the history) on Theory
Transitive_Closure. Suggested NEWS entry:
------------------------------------------------------------------
* Theory Transitive_Closure: Duplicated facts about "relpow" for
"relpowp" to emphasize that both worlds exist and facilitate better
results with "find_theorems".
Added Lemmas:
relpowp_1
relpowp_0_I
relpowp_Suc_I
relpowp_Suc_I2
relpowp_0_E
relpowp_Suc_E
relpowp_E
relpowp_Suc_D2
relpowp_Suc_E2
relpowp_Suc_D2'
relpowp_E2
relpowp_add
relpowp_commute
relpowp_bot
rtranclp_imp_Sup_relpowp
relpowp_imp_rtranclp
rtranclp_is_Sup_relpowp
rtranclp_power
tranclp_power
rtranclp_imp_relpowp
relpowp_fun_conv
------------------------------------------------------------------
I pushed your changes to the public repository, but I did not consider
the NEWS entry worth mentioning -- we add theorems on a daily basis,
without explicitly advertising them in the NEWS.
Lukas
cheers
chris
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
