src/Tools/isac/Knowledge/Biegelinie.thy
changeset 60777 df8636ffd6f8
parent 60767 466f0a5bfb73
     1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Sun Dec 10 07:56:02 2023 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Sun Dec 10 17:35:07 2023 +0100
     1.3 @@ -113,7 +113,7 @@
     1.4    E.g. for "Traegerlaenge" in the problem we had "l_l", while in the method we had "beam".
     1.5    This had been working with the old "fun arguments_from_model, relate_args" in LItool.
     1.6    But the Pre_Conds of Biegelinie were empty at that time --
     1.7 -  -- how should this work with Pre_Conds <>[] involved with both, problem and method?
     1.8 +  -- how should this work with Pre_Conds <> [] involved with both, problem and method?
     1.9    A kind of "model-translation" (see the old "fun LItool.arguments_from_model";
    1.10    there is already an implicit kind of relation exploitet by refinement)?
    1.11    In this changeset there is the decision to make the two models equal, of model and of method.
    1.12 @@ -345,7 +345,7 @@
    1.13      "FunktionsVariable fun_var" "AbleitungBiegelinie id_der" "Biegemoment id_momentum"
    1.14      "Querkraft id_lat_force"
    1.15    (* Item for Problem "LINEAR/system", which by [''no_met''] involves refinement *)
    1.16 -    "GleichungsVariablen vs"(*NEW*)
    1.17 +    "GleichungsVariablen vs"
    1.18    Find: "Biegelinie b_b"
    1.19  
    1.20  method met_biege_intconst_2 : "IntegrierenUndKonstanteBestimmen/2xIntegrieren" =