equal
deleted
inserted
replaced
19 "----------- ### thes2file ... Exception- Match raised -----------"; |
19 "----------- ### thes2file ... Exception- Match raised -----------"; |
20 "----------- search for data error in thes2file ------------------"; |
20 "----------- search for data error in thes2file ------------------"; |
21 "----------- thes2file: thy_containing_rls : rls '...' not in ! --"; |
21 "----------- thes2file: thy_containing_rls : rls '...' not in ! --"; |
22 "----------- fun Thm.make_thm ------------------------------------"; |
22 "----------- fun Thm.make_thm ------------------------------------"; |
23 "----------- correct theIDs for e_rls ----------------------------"; |
23 "----------- correct theIDs for e_rls ----------------------------"; |
24 "----------- correct theIDs for list_rls -------------------------"; |
|
25 "----------- fun revert_sym --------------------------------------"; |
24 "----------- fun revert_sym --------------------------------------"; |
26 "----------- fun thms_of_rlss ------------------------------------"; |
25 "----------- fun thms_of_rlss ------------------------------------"; |
27 "----------- repair thydata2xml for rls --------------------------"; |
26 "----------- repair thydata2xml for rls --------------------------"; |
28 "-----------------------------------------------------------------"; |
27 "-----------------------------------------------------------------"; |
29 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy"; |
28 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy"; |
166 else error "thy_containing_rls e_rls changed"; |
165 else error "thy_containing_rls e_rls changed"; |
167 show_thes (); |
166 show_thes (); |
168 (*shows different assignment for "e_rls"... |
167 (*shows different assignment for "e_rls"... |
169 : |
168 : |
170 ["IsacScripts", "KEStore", "Rulesets", "e_rls"], |
169 ["IsacScripts", "KEStore", "Rulesets", "e_rls"], |
171 :*) |
|
172 |
|
173 "----------- correct theIDs for list_rls -------------------------"; |
|
174 "----------- correct theIDs for list_rls -------------------------"; |
|
175 "----------- correct theIDs for list_rls -------------------------"; |
|
176 if thy_containing_rls "Build_Thydata" "list_rls" = ("IsacScripts", "Atools") then () |
|
177 else error "thy_containing_rls list_rls changed"; |
|
178 show_thes (); |
|
179 (*shows different assignment for "list_rls"... |
|
180 : |
|
181 ["IsacScripts", "Tools", "Rulesets", "list_rls"], |
|
182 :*) |
170 :*) |
183 |
171 |
184 "----------- fun revert_sym --------------------------------------"; |
172 "----------- fun revert_sym --------------------------------------"; |
185 "----------- fun revert_sym --------------------------------------"; |
173 "----------- fun revert_sym --------------------------------------"; |
186 "----------- fun revert_sym --------------------------------------"; |
174 "----------- fun revert_sym --------------------------------------"; |