Tue, 10 Aug 2021 12:58:33 +0200explain "KEStore_Elems.add_thes" in TODO.md
wneuper <walther.neuper@jku.at> [Tue, 10 Aug 2021 12:58:33 +0200] rev 60365
explain "KEStore_Elems.add_thes" in TODO.md

Tue, 10 Aug 2021 12:56:06 +0200cleanup MethodC.prep_input that used a different theory
wneuper <walther.neuper@jku.at> [Tue, 10 Aug 2021 12:56:06 +0200] rev 60364
cleanup MethodC.prep_input that used a different theory

Tue, 10 Aug 2021 11:55:24 +0200tuned
wneuper <walther.neuper@jku.at> [Tue, 10 Aug 2021 11:55:24 +0200] rev 60363
tuned

Tue, 10 Aug 2021 11:54:12 +0200relate note on planned improvements (cf.03dea0a179d0) to TODO.md
wneuper <walther.neuper@jku.at> [Tue, 10 Aug 2021 11:54:12 +0200] rev 60362
relate note on planned improvements (cf.03dea0a179d0) to TODO.md

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