wneuper <walther.neuper@jku.at> [Sun, 26 Sep 2021 20:58:57 +0200] rev 60410
another simp rule missing; lemma realpow_uminus_simps fails.
wenzelm [Sat, 25 Sep 2021 21:41:51 +0200] rev 60409
more simp rules: 1 is another special case, so (- 1) needs to be treated separately;
wneuper <walther.neuper@jku.at> [Sat, 25 Sep 2021 13:54:06 +0200] rev 60408
\\ uncovered corner case of realpow: (- 1) ? 2
wenzelm [Fri, 24 Sep 2021 14:18:10 +0200] rev 60407
proper simp_ctxt;
wneuper <walther.neuper@jku.at> [Thu, 23 Sep 2021 13:47:16 +0200] rev 60406
\\ realpow is not handled by present Simplifier.rewrite simp_ctxt
wenzelm [Thu, 16 Sep 2021 17:23:54 +0200] rev 60405
separate realpow constant, with additional cases not covered by Transcendental.powr;
wenzelm [Thu, 16 Sep 2021 12:23:57 +0200] rev 60404
adapted to Isabelle/c645d973f881;
wenzelm [Thu, 16 Sep 2021 11:47:03 +0200] rev 60403
follow Isabelle repository;
wneuper <walther.neuper@jku.at> [Tue, 14 Sep 2021 16:06:42 +0200] rev 60402
\\adopt Isabelles calculation of numerals, "(- 1) ? 2" still missing
wneuper <walther.neuper@jku.at> [Tue, 14 Sep 2021 12:22:57 +0200] rev 60401
\\adopt Isabelles calculation of numerals, some cases are missing