diff -r ba408e905cce -r c0fe04973189 src/Tools/isac/Knowledge/Biegelinie.thy
--- a/src/Tools/isac/Knowledge/Biegelinie.thy	Wed Apr 04 12:41:03 2018 +0200
+++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Wed Apr 11 14:44:46 2018 +0200
@@ -184,6 +184,10 @@
 	 scr = Rule.EmptyScr};
 *}
 
+section \<open>Methods\<close>
+
+subsection \<open>Sub-problem "integrate and determine constants", little modularisation\<close>
+
 setup {* KEStore_Elems.add_mets
   [Specify.prep_met @{theory} "met_biege" [] Celem.e_metID 
 	    (["IntegrierenUndKonstanteBestimmen"],
@@ -260,13 +264,43 @@
           "       B__B = Take  B__B;                                               " ^
           "       B__B = ((Substitute c_1_2) @@                                    " ^
           "              (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
-          " in B__B)"),
-    Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID
+          " in B__B)")]
+*}
+subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>
+(*------------------------------------------------------------------------------------\\\ 
+consts
+  Biegelinie' :: ID  vonBelastungZu :: ID  Biegelinien :: ID  ausBelastung :: ID     
+  setzeRandbedingungen :: ID  setzeRandbedingungenEin :: ID  LINEAR :: ID  system :: ID
+  no_met :: ID  make_ratpoly_in :: ID          
+  bdv :: real  c :: real  c_2 :: real  c_3 :: real  c_4 :: real
+
+partial_function (tailrec) biegelinie ::
+  "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool"
+where
+  "biegelinie l q v b s = 
+    (let                                                                             
+      funs = (SubProblem (Biegelinie',                                               
+        [vonBelastungZu, Biegelinien], [Biegelinien, ausBelastung])                  
+        [REAL q, REAL v]);                                                           
+      equs = (SubProblem (Biegelinie',                                               
+        [setzeRandbedingungen, Biegelinien], [Biegelinien, setzeRandbedingungenEin]) 
+        [BOOL_LIST funs, BOOL_LIST s]);                                              
+      cons = (SubProblem (Biegelinie', [LINEAR, system], [no_met])                   
+        [BOOL_LIST equs, REAL_LIST [c, c_2, c_3, c_4]]);                             
+      B = Take (lastI funs);                                                         
+      B = ((Substitute cons) @@                                                      
+            (Rewrite_Set_Inst [(bdv, v)] make_ratpoly_in False)) B                  
+    in B)                                                                           "
+
+ \\\------------------------------------------------------------------------------------*)
+
+setup {* KEStore_Elems.add_mets
+  [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID
 	    (["IntegrierenUndKonstanteBestimmen2"],
-	      [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
-		      (*("#Where",["0 < l_l"]), ...wait for &lt; and handling Arbfix*)
-		      ("#Find"  ,["Biegelinie b_b"]),
-		      ("#Relate",["Randbedingungen r_b"])],
+	      [("#Given" ,["Traegerlaenge l", "Streckenlast q", "FunktionsVariable v"]),
+		      (*("#Where",["0 < l"]), ...wait for &lt; and handling Arbfix*)
+		      ("#Find"  ,["Biegelinie b"]),
+		      ("#Relate",["Randbedingungen s"])],
 	      {rew_ord'="tless_true", 
 	        rls' = Rule.append_rls "erls_IntegrierenUndK.." Rule.e_rls 
 				      [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
@@ -280,24 +314,22 @@
 				        Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
 				        Rule.Thm ("if_False",TermC.num_str @{thm if_False})],
 				  prls = Rule.Erls, crls = Atools_erls, errpats = [], nrls = Rule.Erls},
-        "Script Biegelinie2Script                                                  " ^
-          "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
-          "  (let                                                                    " ^
-          "      (fun_s:: bool list) =                                               " ^
-          "             (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien],       " ^
-          "                          [Biegelinien,ausBelastung])                     " ^
-          "                          [REAL q__q, REAL v_v]);                         " ^
-          "      (equ_s::bool list) =                                                " ^
-          "             (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien], " ^
-          "                          [Biegelinien,setzeRandbedingungenEin])          " ^
-          "                          [BOOL_LIST fun_s, BOOL_LIST r_b]);              " ^
-          "      (con_s::bool list) =                                                " ^
-          "             (SubProblem (Biegelinie',[LINEAR,system],[no_met])           " ^
-          "                          [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]);  " ^
-          "       B_B = Take (lastI fun_s);                                          " ^
-          "       B_B = ((Substitute con_s) @@                                       " ^
-          "              (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B  " ^
-          " in B_B)"),
+        "Script Biegelinie2Script                                                           " ^
+        "(l::real) (q :: real) (v :: real) (b :: real => real) (s :: bool list) =           " ^
+        "  (let                                                                             " ^
+        "    (funs :: bool list) = (SubProblem (Biegelinie',                                " ^
+        "      [vonBelastungZu, Biegelinien], [Biegelinien, ausBelastung])                  " ^
+        "      [REAL q, REAL v]);                                                           " ^
+        "    (equs :: bool list) = (SubProblem (Biegelinie',                                " ^
+        "      [setzeRandbedingungen, Biegelinien], [Biegelinien, setzeRandbedingungenEin]) " ^
+        "      [BOOL_LIST funs, BOOL_LIST s]);                                              " ^
+        "    (cons :: bool list) = (SubProblem (Biegelinie',                                " ^
+        "      [LINEAR, system], [no_met])                                                  " ^
+        "      [BOOL_LIST equs, REAL_LIST [c, c_2, c_3, c_4]]);                             " ^
+        "    B = Take (lastI funs);                                                         " ^
+        "    B = ((Substitute cons) @@                                                      " ^
+        "           (Rewrite_Set_Inst [(bdv, v)] make_ratpoly_in False)) B                  " ^
+        "  in B)                                                                           "),
     Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID
 	    (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
 	      {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
@@ -317,8 +349,12 @@
 	    (["Biegelinien"], [],
 	      {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
           errpats = [], nrls = Rule.e_rls},
-        "empty_script"),
-    Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
+        "empty_script")]
+*}
+subsection \<open>Compute the general bending line\<close>
+
+setup {* KEStore_Elems.add_mets
+  [Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
 	    (["Biegelinien", "ausBelastung"],
 	      [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
 	        ("#Find"  ,["Funktionen fun_s"])],
@@ -354,8 +390,12 @@
           "             (SubProblem (Biegelinie',[named,integrate,function],      " ^
           "                          [diff,integration,named])                    " ^
           "                          [REAL (rhs N__N), REAL v_v, REAL_REAL y])    " ^
-          " in [Q__Q, M__M, N__N, B__B])"),
-    Specify.prep_met @{theory} "met_biege_setzrand" [] Celem.e_metID
+          " in [Q__Q, M__M, N__N, B__B])")]
+*}
+subsection \<open>Substitute the constraints into the equations\<close>
+
+setup {* KEStore_Elems.add_mets
+  [Specify.prep_met @{theory} "met_biege_setzrand" [] Celem.e_metID
 	    (["Biegelinien", "setzeRandbedingungenEin"],
 	      [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
 	        ("#Find"  , ["Gleichungen equs'''"])],
@@ -413,8 +453,12 @@
           "             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
           "                          [Equation,fromFunction])              " ^
           "                          [BOOL (hd f_s), BOOL b_4])          " ^
-          " in [e_1,e_2,e_3,e_4])"*)),
-    Specify.prep_met @{theory} "met_equ_fromfun" [] Celem.e_metID
+          " in [e_1,e_2,e_3,e_4])"*))]
+*}
+subsection \<open>Transform an equality into a function\<close>
+
+setup {* KEStore_Elems.add_mets
+  [Specify.prep_met @{theory} "met_equ_fromfun" [] Celem.e_metID
 	    (["Equation","fromFunction"],
 	      [("#Given" ,["functionEq fu_n","substitution su_b"]),
 	        ("#Find"  ,["equality equ'''"])],