equal
deleted
inserted
replaced
68 ; |
68 ; |
69 if Thy_Read.thy_containing_rls "Biegelinie" "empty" = ("IsacScripts", "Know_Store") then () |
69 if Thy_Read.thy_containing_rls "Biegelinie" "empty" = ("IsacScripts", "Know_Store") then () |
70 else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'e_rls'") |
70 else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'e_rls'") |
71 ; |
71 ; |
72 if Thy_Read.thy_containing_rls "Build_Thydata" "prog_expr" = (*FIXME: handle redifinition in several thys*) |
72 if Thy_Read.thy_containing_rls "Build_Thydata" "prog_expr" = (*FIXME: handle redifinition in several thys*) |
73 ("IsacKnowledge", "Base_Tools") then () |
73 (*("IsacKnowledge", "Base_Tools") ...before session Isac builds on SPARK ?!?*) |
74 else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'prog_expr'") |
74 ("IsacScripts", "Prog_Expr") |
|
75 then () else error ("Thy_Read.thy_containing_rls changed for 'Biegelinie', 'prog_expr'") |
75 |
76 |
76 "----------- fun thy_containing_cal ---------------------"; |
77 "----------- fun thy_containing_cal ---------------------"; |
77 "----------- fun thy_containing_cal ---------------------"; |
78 "----------- fun thy_containing_cal ---------------------"; |
78 "----------- fun thy_containing_cal ---------------------"; |
79 "----------- fun thy_containing_cal ---------------------"; |
79 (* ATTENTION: both, "IsacKnowledge" and "Prog_Expr" are fixed as results for any input*) |
80 (* ATTENTION: both, "IsacKnowledge" and "Prog_Expr" are fixed as results for any input*) |