<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
On 04/16/2012 09:13 AM, Christian Sternagel wrote:
<blockquote cite="mid:4F8BC6A4.2050501@jaist.ac.jp" type="cite">Hi
all,
<br>
<br>
On 04/03/2012 02:51 AM, Florian Haftmann wrote:
<br>
<blockquote type="cite">well, I suggest to augment the existing
theory with lemmas transferred
<br>
from relpow to relpowp to emphasize that both worlds exists and
that
<br>
lemmas can be found easier by find_theorems. The typical
pattern is
<br>
<br>
lemma foo_relpow: …
<br>
<proof>
<br>
<br>
lemma foo_relpowp: …
<br>
by (fact foo_relpow [to_pred])
<br>
<br>
</blockquote>
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:
<br>
<br>
</blockquote>
I am testing it again, cf.
<a class="moz-txt-link-freetext" href="http://isabelle.in.tum.de/testboard/Isabelle/rev/74e9843f7aae">http://isabelle.in.tum.de/testboard/Isabelle/rev/74e9843f7aae</a><br>
<br>
Lukas<br>
<blockquote cite="mid:4F8BC6A4.2050501@jaist.ac.jp" type="cite">------------------------------------------------------------------
<br>
* Theory Transitive_Closure: Duplicated facts about "relpow" for
"relpowp" to emphasize that both worlds exist and facilitate
better results with "find_theorems".
<br>
<br>
Added Lemmas:
<br>
relpowp_1
<br>
relpowp_0_I
<br>
relpowp_Suc_I
<br>
relpowp_Suc_I2
<br>
relpowp_0_E
<br>
relpowp_Suc_E
<br>
relpowp_E
<br>
relpowp_Suc_D2
<br>
relpowp_Suc_E2
<br>
relpowp_Suc_D2'
<br>
relpowp_E2
<br>
relpowp_add
<br>
relpowp_commute
<br>
relpowp_bot
<br>
rtranclp_imp_Sup_relpowp
<br>
relpowp_imp_rtranclp
<br>
rtranclp_is_Sup_relpowp
<br>
rtranclp_power
<br>
tranclp_power
<br>
rtranclp_imp_relpowp
<br>
relpowp_fun_conv
<br>
------------------------------------------------------------------
<br>
<br>
cheers
<br>
<br>
chris
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>