Walther Neuper <neuper@ist.tugraz.at> [Sun, 22 Sep 2013 18:29:15 +0200] rev 52127
error in last changeset removed
Walther Neuper <neuper@ist.tugraz.at> [Sun, 22 Sep 2013 18:17:25 +0200] rev 52126
narrow behaviour of Theory_Data and "ruleset' = Unsynchronized.ref"
In order to have KEStore_Elems as similar to the old Unsynchronized.ref,
"fun rls_eq" and future relatives require specific attention.
Walther Neuper <neuper@ist.tugraz.at> [Sun, 22 Sep 2013 18:09:05 +0200] rev 52125
add functions accessing Theory_Data in parallel to those accessing "ruleset' = Unsynchronized.ref"
updates have been done incrementally following Build_Isac.thy:
# ./bin/isabelle jedit -l HOL src/Tools/isac/ProgLang/ProgLang.thy &
# ./bin/isabelle jedit -l HOL src/Tools/isac/Interpret/Interpret.thy &
# ./bin/isabelle jedit -l HOL src/Tools/isac/xmlsrc/xmlsrc.thy &
# ./bin/isabelle jedit -l HOL src/Tools/isac/Frontend/Frontend.thy &
Note, that the original access function "fun assoc_rls" is still outcommented;
so the old and new functionality is established in parallel.
Walther Neuper <neuper@ist.tugraz.at> [Sun, 22 Sep 2013 17:28:55 +0200] rev 52124
shift existing access functions for Unsynchronized.ref to bottom of KEStore.thy
Walther Neuper <neuper@ist.tugraz.at> [Fri, 20 Sep 2013 15:30:09 +0200] rev 52123
tuned
Walther Neuper <neuper@ist.tugraz.at> [Fri, 20 Sep 2013 15:26:24 +0200] rev 52122
add Theory_Data to prepare removal of Unsynchronized.ref
Walther Neuper <neuper@ist.tugraz.at> [Thu, 19 Sep 2013 15:51:03 +0200] rev 52121
restrict access to "ruleset' = Unsynchronized.ref"
to "fun assoc_rls" and "overwritelthy thy (!ruleset'"
Walther Neuper <neuper@ist.tugraz.at> [Thu, 19 Sep 2013 15:45:07 +0200] rev 52120
tuned
Walther Neuper <neuper@ist.tugraz.at> [Thu, 19 Sep 2013 13:37:26 +0200] rev 52119
added some existing tests
Walther Neuper <neuper@ist.tugraz.at> [Thu, 19 Sep 2013 13:26:21 +0200] rev 52118
prepare removing Unsynchronized.ref, final version
no (efficient) way to avoid duplication of Theory_Data