1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Thu May 30 12:39:13 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Sat Jun 01 11:09:19 2019 +0200
     1.3 @@ -188,12 +188,13 @@
     1.4  \<close>
     1.5  subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>
     1.6  
     1.7 -partial_function (tailrec) biegelinie :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> real list \<Rightarrow> bool"
     1.8 +partial_function (tailrec) biegelinie ::
     1.9 +  "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> real list \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
    1.10    where
    1.11 -"biegelinie l q v b s vs =
    1.12 +"biegelinie l q v b s vs id_abl =
    1.13    (let
    1.14      funs = SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
    1.15 -             [''Biegelinien'', ''ausBelastung'']) [REAL q, REAL v];                \<comment> \<open>PROG +args\<close>
    1.16 +             [''Biegelinien'', ''ausBelastung'']) [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl];
    1.17      equs = SubProblem (''Biegelinie'', [''setzeRandbedingungen'', ''Biegelinien''],
    1.18               [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST s];
    1.19      cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''], [''no_met''])
    1.20 @@ -279,10 +280,10 @@
    1.21                 (Rewrite ''make_fun_explicit'' False)) M__M;
    1.22         N__N = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
    1.23                    [''diff'', ''integration'', ''named''])
    1.24 -                [REAL (rhs N__N), REAL v_v, REAL_REAL id_abl];                        \<comment> \<open>PROG string\<close>
    1.25 +                [REAL (rhs N__N), REAL v_v, REAL_REAL id_abl];
    1.26         B__B = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
    1.27                    [''diff'', ''integration'', ''named'']) 
    1.28 -                [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun]                          \<comment> \<open>PROG string\<close>
    1.29 +                [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun]
    1.30   in [Q__Q, M__M, N__N, B__B])"
    1.31  setup \<open>KEStore_Elems.add_mets
    1.32      [Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
    1.33 @@ -445,6 +446,8 @@
    1.34          "      eq_u = (Substitute [su_b]) eq_u               " ^
    1.35          " in (Rewrite_Set ''norm_Rational'' False) eq_u)         "*))]
    1.36  \<close>
    1.37 -
    1.38 +ML \<open>
    1.39 +\<close> ML \<open>
    1.40 +\<close>
    1.41  end
    1.42