equal
deleted
inserted
replaced
36 val bl = [("e_rls",e_rls),("e_rrls",e_rrls)]; |
36 val bl = [("e_rls",e_rls),("e_rrls",e_rrls)]; |
37 val b = ("e_rls",("Atools",e_rrls)); |
37 val b = ("e_rls",("Atools",e_rrls)); |
38 overwrite (al, b); |
38 overwrite (al, b); |
39 overwritelthy thy (al, bl); |
39 overwritelthy thy (al, bl); |
40 |
40 |
41 case assoc' ((KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")),"e_rls") of |
41 case assoc' ((Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")),"e_rls") of |
42 SOME ("Tools", Rls _) => () |
42 SOME ("Tools", Rls _) => () |
43 | _ => error "e_rls not in Theory_Data" |
43 | _ => error "e_rls not in Theory_Data" |
44 |
44 |
45 assoc_rls "e_rls"; |
45 assoc_rls "e_rls"; |
46 |
46 |
78 makeHrls "IsacKnowledge" ("integration_rules", (thy', integration_rules)); |
78 makeHrls "IsacKnowledge" ("integration_rules", (thy', integration_rules)); |
79 |
79 |
80 val thy' = "Test"; |
80 val thy' = "Test"; |
81 val rlss = filter ((curry op= thy') o |
81 val rlss = filter ((curry op= thy') o |
82 ((#1 o #2):(rls' * (theory' * rls)) -> theory')) |
82 ((#1 o #2):(rls' * (theory' * rls)) -> theory')) |
83 (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")); |
83 (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")); |
84 collect_rlss ("IsacKnowledge",thy'); |
84 collect_rlss ("IsacKnowledge",thy'); |
85 |
85 |
86 "collect_thy thy-------------------------------------------------"; |
86 "collect_thy thy-------------------------------------------------"; |
87 val thy' = "ListC"; |
87 val thy' = "ListC"; |
88 val thy = assoc_thy (thyID2theory' thy'); |
88 val thy = assoc_thy (thyID2theory' thy'); |
386 then () else error "thy_containing_rls changed ancestors_rls for (Poly, discard_minus)"; |
386 then () else error "thy_containing_rls changed ancestors_rls for (Poly, discard_minus)"; |
387 |
387 |
388 val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list; |
388 val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list; |
389 val ancestors_rls = |
389 val ancestors_rls = |
390 filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory')) |
390 filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory')) |
391 (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))); |
391 (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))); |
392 |
392 |
393 case assoc (ancestors_rls, rls') of |
393 case assoc (ancestors_rls, rls') of |
394 SOME ("Poly", Rls {id = "discard_minus", ...}) => () |
394 SOME ("Poly", Rls {id = "discard_minus", ...}) => () |
395 | _ => error "thy_containing_rls changed 2"; |
395 | _ => error "thy_containing_rls changed 2"; |
396 |
396 |