Walther Neuper <neuper@ist.tugraz.at> [Mon, 21 Oct 2013 09:28:01 +0200] rev 52149
removed unused code
Walther Neuper <neuper@ist.tugraz.at> [Mon, 21 Oct 2013 09:03:50 +0200] rev 52148
"axiomatization" replaces "axioms" preparing for Isabelle2013-1
Note the text at begin of ListC.thy
Walther Neuper <neuper@ist.tugraz.at> [Fri, 18 Oct 2013 14:36:51 +0200] rev 52147
merged
Walther Neuper <neuper@ist.tugraz.at> [Fri, 18 Oct 2013 14:36:33 +0200] rev 52146
some clean-ups
Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at> [Wed, 16 Oct 2013 23:59:43 +0100] rev 52145
add functions accessing Theory_Data in parallel to those accessing "calclist' = Unsynchronized.ref
Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at> [Thu, 10 Oct 2013 19:16:16 +0100] rev 52144
restrict access to "calclist' = Unsynchronized.ref"
to assoc_calc, assoc_calc' and overwritel
Walther Neuper <neuper@ist.tugraz.at> [Mon, 30 Sep 2013 16:42:52 +0200] rev 52143
survey on transition from "ruleset' = Unsynchronized.ref" to Theory_Data
In order to keep Test_Isac running at each commit, the transition
was separated into these steps
(1) restrict access to "ruleset' = Unsynchronized.ref", 9690a8d5f1c0
(2) add functions accessing Theory_Data in parallel to those accessing "ruleset' = Unsynchronized.ref", 6f1d3415dc68
(3) narrow data of Theory_Data and "ruleset' = Unsynchronized.ref", 47995aefb1c9
(4) check differences between Theory_Data and "ruleset' = Unsynchronized.ref", 0e2d1a46236d
(5) iterate steps (3) and (4), ef98c3e15a8d, 9d1568e89775, 90546fa8b868
(6) switch from "ruleset' = Unsynchronized.ref" to Theory_Data
(7) remove all code concerned with "ruleset' = Unsynchronized.ref" and with transition; this will be done in a subsequent changeset.
The Unsynchronized.ref outlined in this changeset shall be tackled the same way.
Walther Neuper <neuper@ist.tugraz.at> [Mon, 30 Sep 2013 16:22:07 +0200] rev 52142
switched from "ruleset' = Unsynchronized.ref" to Theory_Data
After thorough narrowing of data stored respectively,
seven final updates (marked with SWITCH) were successful.
Running Build_Isac and Test_Isac showed, that Unsynchronized.ref
is more pervasive than Theory_Data; the following adaptions were done:
# a variant of "fun assoc_rls'" uses the current theory instead Isac
# ruleset "erls" was not available in test/../diff.sml
Walther Neuper <neuper@ist.tugraz.at> [Mon, 30 Sep 2013 11:50:13 +0200] rev 52141
last difference between Theory_Data and "ruleset' = Unsynchronized.ref" removed
Output created by top of Build_Thydata.thy shows no more differences (in log/Isac)
beyond a different sequence of entries to Unsynchronized.ref | KEStore
A new test covers the implicitly executed merge_rlss.
Reasons for changed tests in test/../polyeq.sml and rootrat.sml are unclear.
Walther Neuper <neuper@ist.tugraz.at> [Sun, 29 Sep 2013 18:48:35 +0200] rev 52140
Thy_Info.get_theory doesn't reliably know ancestor theories
... for a theory dynamically loaded --- which is different from building sessions.
See https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-September/msg00060.html