wneuper <walther.neuper@jku.at> [Mon, 19 Jul 2021 18:29:46 +0200] rev 60337
cleanup after "eliminate ThmC.numerals_to_Free"
wneuper <walther.neuper@jku.at> [Mon, 19 Jul 2021 17:29:35 +0200] rev 60336
introduce ALL valid const_name in test/*
wneuper <walther.neuper@jku.at> [Mon, 19 Jul 2021 15:34:54 +0200] rev 60335
ALL const_name replaces (others cannot be replaced)
wneuper <walther.neuper@jku.at> [Sun, 18 Jul 2021 21:19:25 +0200] rev 60334
Test_Some.the works, too
wneuper <walther.neuper@jku.at> [Sun, 18 Jul 2021 21:15:21 +0200] rev 60333
Test_Isac_Short.thy, Test_Some.the work on new src, new TOODOOs
notes
# the previous changeset run Test_Isac_Short.thy on src/* from before the merge
# errors coming from merge are outcommented with TOODOO
wneuper <walther.neuper@jku.at> [Sun, 18 Jul 2021 18:30:09 +0200] rev 60332
Test_Isac_Short.thy works again (ndefined ML antiquotation: "rule_thm_sym", "rule_thm")
wneuper <walther.neuper@jku.at> [Sun, 18 Jul 2021 18:15:27 +0200] rev 60331
merged
wneuper <walther.neuper@jku.at> [Sun, 18 Jul 2021 16:20:32 +0200] rev 60330
eliminate ThmC.numerals_to_Free: Test_Isac_Short.thy works with TOODOO s
wneuper <walther.neuper@jku.at> [Sat, 17 Jul 2021 14:05:28 +0200] rev 60329
replace "-*" by "- *" for numerals "*" in test/*
wneuper <walther.neuper@jku.at> [Fri, 16 Jul 2021 07:45:06 +0200] rev 60328
separate poly-1 /-2.sml