Walther Neuper <walther.neuper@jku.at> [Thu, 26 Mar 2020 16:17:21 +0100] rev 59841
improve classification of assumptions (True, False, indeterminate)
Walther Neuper <walther.neuper@jku.at> [Wed, 25 Mar 2020 11:01:02 +0100] rev 59840
remove unused field in Ctree, finish
Walther Neuper <walther.neuper@jku.at> [Wed, 25 Mar 2020 10:38:31 +0100] rev 59839
remove unused field in Ctree
note: same 2 errors as before in Test_Isac_Short
Walther Neuper <walther.neuper@jku.at> [Wed, 25 Mar 2020 09:38:40 +0100] rev 59838
cleanup LItool.resume_prog, cf.edf1643edde5
note: same 2 ?!? errors as before
Walther Neuper <walther.neuper@jku.at> [Wed, 25 Mar 2020 09:17:05 +0100] rev 59837
ONE tactic per step VISIBLE in calculation
Test_Some_Short.thy has 2 errors, which disappear in thy ?!?:
ML_file "Interpret/error-pattern.sml" Undefined fact: "all_left"
ML_file "Knowledge/inssort.sml" Undefined fact: "xfoldr_Nil"
Walther Neuper <walther.neuper@jku.at> [Tue, 24 Mar 2020 17:01:02 +0100] rev 59836
prep. ONE tactic per step VISIBLE in calculation
note: there were exceptions: Take and Subproblem as
first tactics in a (sub-)calculation.
Walther Neuper <walther.neuper@jku.at> [Mon, 23 Mar 2020 17:51:35 +0100] rev 59835
make Check_elementwise' idle wrt. Calc.T
Note: kept for covering general case in Ctree (step between two Check_Postcond)
Walther Neuper <walther.neuper@jku.at> [Mon, 23 Mar 2020 14:55:34 +0100] rev 59834
start restructuring test/../isac/*
according to
https://isac.miraheze.org/wiki/Policies_for_the_test_suite#Multiple_test_instances_of_one_example
Walther Neuper <walther.neuper@jku.at> [Mon, 23 Mar 2020 13:31:29 +0100] rev 59833
separate structure Detail_Step
Walther Neuper <walther.neuper@jku.at> [Fri, 20 Mar 2020 19:31:55 +0100] rev 59832
collect code for by_tactic..Check_Postcond'
Note: can all Step_Solve.by_tactic transferred to LI.by_tactic ?