Tue, 10 Aug 2021 11:29:33 +0200remove items already done
wneuper <walther.neuper@jku.at> [Tue, 10 Aug 2021 11:29:33 +0200] rev 60361
remove items already done

Tue, 10 Aug 2021 11:01:18 +0200eliminate ThyC.to_ctxt, use Proof_Context.init_global inline
wneuper <walther.neuper@jku.at> [Tue, 10 Aug 2021 11:01:18 +0200] rev 60360
eliminate ThyC.to_ctxt, use Proof_Context.init_global inline

Tue, 10 Aug 2021 10:27:15 +0200note on CS c7b1a99bcfd2 , \<^ML>?Thy_Info.get_theory?
wneuper <walther.neuper@jku.at> [Tue, 10 Aug 2021 10:27:15 +0200] rev 60359
note on CS c7b1a99bcfd2 , \<^ML>?Thy_Info.get_theory?

Tue, 10 Aug 2021 09:43:07 +0200complete replacement of Rule.Thm/Eval by \<^rule_thm> and \<^rule_eval> in src/*
wneuper <walther.neuper@jku.at> [Tue, 10 Aug 2021 09:43:07 +0200] rev 60358
complete replacement of Rule.Thm/Eval by \<^rule_thm> and \<^rule_eval> in src/*

Mon, 09 Aug 2021 14:20:20 +0200eliminate ThyC.to_ctxt done except 1 error
wneuper <walther.neuper@jku.at> [Mon, 09 Aug 2021 14:20:20 +0200] rev 60357
eliminate ThyC.to_ctxt done except 1 error

Mon, 09 Aug 2021 11:19:25 +0200remove TOODOOs
wneuper <walther.neuper@jku.at> [Mon, 09 Aug 2021 11:19:25 +0200] rev 60356
remove TOODOOs

Sun, 08 Aug 2021 15:21:33 +0200repair fun is_ratpolyexp
wneuper <walther.neuper@jku.at> [Sun, 08 Aug 2021 15:21:33 +0200] rev 60355
repair fun is_ratpolyexp

Fri, 06 Aug 2021 18:27:05 +0200cleanup files on GCD/gcd
wneuper <walther.neuper@jku.at> [Fri, 06 Aug 2021 18:27:05 +0200] rev 60354
cleanup files on GCD/gcd

Fri, 06 Aug 2021 12:09:06 +0200repair fun order overwritten by previous tests
wneuper <walther.neuper@jku.at> [Fri, 06 Aug 2021 12:09:06 +0200] rev 60353
repair fun order overwritten by previous tests

Fri, 06 Aug 2021 11:13:20 +0200repair (ad-hoc) order in PolyMinus.thy, finished
wneuper <walther.neuper@jku.at> [Fri, 06 Aug 2021 11:13:20 +0200] rev 60352
repair (ad-hoc) order in PolyMinus.thy, finished