equal
deleted
inserted
replaced
189 ############################################################################# |
189 ############################################################################# |
190 # How to manage theorys in subproblems wrt. the requirement, # |
190 # How to manage theorys in subproblems wrt. the requirement, # |
191 # that scripts should be re-usable ? # |
191 # that scripts should be re-usable ? # |
192 ############################################################################# |
192 ############################################################################# |
193 |
193 |
194 eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..' |
194 eg. 'Program Solve_rat_equation' calls 'SubProblem (RatEq',..' |
195 which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script |
195 which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script |
196 because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b |
196 because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b |
197 is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard |
197 is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard |
198 (see match_ags). |
198 (see match_ags). |
199 |
199 |
423 fun merge_rlss (s1, s2) = fold insert_merge_rls s1 s2; |
423 fun merge_rlss (s1, s2) = fold insert_merge_rls s1 s2; |
424 |
424 |
425 |
425 |
426 fun assoc_thy thy = |
426 fun assoc_thy thy = |
427 if thy = "e_domID" |
427 if thy = "e_domID" |
428 then (Rule.Thy_Info_get_theory "Script") (*lower bound of Knowledge*) |
428 then (Rule.Thy_Info_get_theory "Program") (*lower bound of Knowledge*) |
429 else (Rule.Thy_Info_get_theory thy) handle _ => error ("ME_Isa: thy \"" ^ thy ^ "\" not in system"); |
429 else (Rule.Thy_Info_get_theory thy) handle _ => error ("ME_Isa: thy \"" ^ thy ^ "\" not in system"); |
430 |
430 |
431 (* overwrite an element in an association list and pair it with a thyID |
431 (* overwrite an element in an association list and pair it with a thyID |
432 in order to create the thy_hierarchy; |
432 in order to create the thy_hierarchy; |
433 overwrites existing rls' even if they are defined in a different thy; |
433 overwrites existing rls' even if they are defined in a different thy; |