Wed, 29 Sep 2021 19:34:32 +0200unify parse 3: eliminate parseN
wneuper <walther.neuper@jku.at> [Wed, 29 Sep 2021 19:34:32 +0200] rev 60416
unify parse 3: eliminate parseN

Wed, 29 Sep 2021 19:26:12 +0200unify parse 2: eliminate parseold
wneuper <walther.neuper@jku.at> [Wed, 29 Sep 2021 19:26:12 +0200] rev 60415
unify parse 2: eliminate parseold

Wed, 29 Sep 2021 18:56:38 +0200unify parse 1: reorder defs
wneuper <walther.neuper@jku.at> [Wed, 29 Sep 2021 18:56:38 +0200] rev 60414
unify parse 1: reorder defs

Mon, 27 Sep 2021 20:24:24 +0200cleanup; all relevant tests work again
wneuper <walther.neuper@jku.at> [Mon, 27 Sep 2021 20:24:24 +0200] rev 60413
cleanup; all relevant tests work again

Mon, 27 Sep 2021 13:17:52 +0200tuned
wneuper <walther.neuper@jku.at> [Mon, 27 Sep 2021 13:17:52 +0200] rev 60412
tuned

Mon, 27 Sep 2021 13:14:09 +0200simp rules for realpow appear complete
wneuper <walther.neuper@jku.at> [Mon, 27 Sep 2021 13:14:09 +0200] rev 60411
simp rules for realpow appear complete

Sun, 26 Sep 2021 20:58:57 +0200another simp rule missing; lemma realpow_uminus_simps fails.
wneuper <walther.neuper@jku.at> [Sun, 26 Sep 2021 20:58:57 +0200] rev 60410
another simp rule missing; lemma realpow_uminus_simps fails.

Sat, 25 Sep 2021 21:41:51 +0200more simp rules: 1 is another special case, so (- 1) needs to be treated separately;
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;

Sat, 25 Sep 2021 13:54:06 +0200\\ uncovered corner case of realpow: (- 1) ? 2
wneuper <walther.neuper@jku.at> [Sat, 25 Sep 2021 13:54:06 +0200] rev 60408
\\ uncovered corner case of realpow: (- 1) ? 2

Fri, 24 Sep 2021 14:18:10 +0200proper simp_ctxt;
wenzelm [Fri, 24 Sep 2021 14:18:10 +0200] rev 60407
proper simp_ctxt;