Walther Neuper <neuper@ist.tugraz.at> [Sat, 31 May 2014 15:53:46 +0200] rev 55416
ad 967c8a1eb6b1 (6): switched from 'thehier = Unsynchronized.ref' to Theory_Data
However, 'thehier :=' is handled later -- different to 967c8a1eb6b1
Walther Neuper <neuper@ist.tugraz.at> [Sat, 31 May 2014 15:09:33 +0200] rev 55415
details on 632d2ecab96f: error (from <NEXT> on new Worksheet)
# inform.sml: fetchErrorpatterns causes same behaviour in Test_Isac;
so the hack has been undone, since it doesn't work anymore.
# tackling the error is postponed to removing "! thehier"
Test_Isac works for e_rls and list_rls in fetchErrorpatterns
Walther Neuper <neuper@ist.tugraz.at> [Thu, 08 May 2014 14:09:02 +0200] rev 55414
reset Polynomial.thy for LaTeXing polypaper
Walther Neuper <neuper@ist.tugraz.at> [Sun, 04 May 2014 14:37:28 +0200] rev 55413
unclear difference Test_Isac.thy -- Test_Some.thy
Walther Neuper <neuper@ist.tugraz.at> [Sun, 04 May 2014 14:02:23 +0200] rev 55412
error (from <NEXT> on new Worksheet) related to thehier
Walther Neuper <neuper@ist.tugraz.at> [Tue, 18 Mar 2014 08:56:41 +0100] rev 55411
notes on how "Generate representations for ISAC Knowledge"
Walther Neuper <neuper@ist.tugraz.at> [Tue, 18 Mar 2014 08:42:45 +0100] rev 55410
generated xml-files from Test_Build_Thydata.thy
next step will be generation of html from xml by java-frontend
Walther Neuper <neuper@ist.tugraz.at> [Tue, 18 Mar 2014 06:36:57 +0100] rev 55409
ad 967c8a1eb6b1 (2): add functions accessing Theory_Data in parallel to thehier
# FIXME the stubs
# FIXME: filter Thm ("inv_...", thm) in "fun thms_of_rlss" ? "fun thms_of_rls"
and handle these avoiding "??unknown"
# FIXME: test/../build_thydata.sml, ../thy-hierarchy.sml are not updated to new
"fun collect_part"
Walther Neuper <neuper@ist.tugraz.at> [Mon, 17 Mar 2014 15:20:15 +0100] rev 55408
re-establish tests for thehier
tests are not all up to date with the re-established
construction of thehier
Walther Neuper <neuper@ist.tugraz.at> [Mon, 17 Mar 2014 13:56:34 +0100] rev 55407
tuned