
diff -r 6d9fb5475156 -r 7d603b7ead73 src/Tools/isac/Knowledge/Biegelinie.thy
--- a/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Sep 09 09:58:28 2010 +0200
+++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Sep 09 13:31:36 2010 +0200
@@ -1,7 +1,6 @@
 (* chapter 'Biegelinie' from the textbook: 
    Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271.
-   author: Walther Neuper
-   050826,
+   author: Walther Neuper 050826,
    (c) due to copyright terms
 *)
 
@@ -9,29 +8,29 @@
 
 consts
 
-  q_    :: real => real ("q'_")     (* Streckenlast               *)
-  Q     :: real => real             (* Querkraft                  *)
-  Q'    :: real => real             (* Ableitung der Querkraft    *)
-  M'_b  :: real => real ("M'_b")    (* Biegemoment                *)
-  M'_b' :: real => real ("M'_b'")   (* Ableitung des Biegemoments *)
-  y''   :: real => real             (* 2.Ableitung der Biegeline  *)
-  y'    :: real => real             (* Neigung der Biegeline      *)
-(*y     :: real => real             (* Biegeline                  *)*)
-  EI    :: real                     (* Biegesteifigkeit           *)
+  q_    :: "real => real" ("q'_")     (* Streckenlast               *)
+  Q     :: "real => real"             (* Querkraft                  *)
+  Q'    :: "real => real"             (* Ableitung der Querkraft    *)
+  M'_b  :: "real => real" ("M'_b")    (* Biegemoment                *)
+  M'_b' :: "real => real" ("M'_b'")   (* Ableitung des Biegemoments *)
+  y''   :: "real => real"             (* 2.Ableitung der Biegeline  *)
+  y'    :: "real => real"             (* Neigung der Biegeline      *)
+(*y     :: "real => real"             (* Biegeline                  *)*)
+  EI    :: "real"                     (* Biegesteifigkeit           *)
 
   (*new Descriptions in the related problems*)
-  Traegerlaenge            :: real => una
-  Streckenlast             :: real => una
-  BiegemomentVerlauf       :: bool => una
-  Biegelinie               :: (real => real) => una
-  Randbedingungen          :: bool list => una
-  RandbedingungenBiegung   :: bool list => una
-  RandbedingungenNeigung   :: bool list => una
-  RandbedingungenMoment    :: bool list => una
-  RandbedingungenQuerkraft :: bool list => una
-  FunktionsVariable        :: real => una
-  Funktionen               :: bool list => una
-  Gleichungen              :: bool list => una
+  Traegerlaenge            :: "real => una"
+  Streckenlast             :: "real => una"
+  BiegemomentVerlauf       :: "bool => una"
+  Biegelinie               :: "(real => real) => una"
+  Randbedingungen          :: "bool list => una"
+  RandbedingungenBiegung   :: "bool list => una"
+  RandbedingungenNeigung   :: "bool list => una"
+  RandbedingungenMoment    :: "bool list => una"
+  RandbedingungenQuerkraft :: "bool list => una"
+  FunktionsVariable        :: "real => una"
+  Funktionen               :: "bool list => una"
+  Gleichungen              :: "bool list => una"
 
   (*Script-names*)
   Biegelinie2Script        :: "[real,real,real,real=>real,bool list,
@@ -81,31 +80,32 @@
 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
 store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"] 
 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
-store_thm thy ("Belastung_Querkraft", Belastung_Querkraft)
+store_thm thy ("Belastung_Querkraft", @{thm Belastung_Querkraft})
 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
-store_thm thy ("Moment_Neigung", Moment_Neigung)
+store_thm thy ("Moment_Neigung", @{thm Moment_Neigung})
 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
-store_thm thy ("Moment_Querkraft", Moment_Querkraft)
+store_thm thy ("Moment_Querkraft", @{thm Moment_Querkraft})
 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
-store_thm thy ("Neigung_Moment", Neigung_Moment)
+store_thm thy ("Neigung_Moment", @{thm Neigung_Moment})
 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
-store_thm thy ("Querkraft_Belastung", Querkraft_Belastung)
+store_thm thy ("Querkraft_Belastung", @{thm Querkraft_Belastung})
 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
-store_thm thy ("Querkraft_Moment", Querkraft_Moment)
+store_thm thy ("Querkraft_Moment", @{thm Querkraft_Moment})
 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
-store_thm thy ("make_fun_explicit", make_fun_explicit)
+store_thm thy ("make_fun_explicit", @{thm make_fun_explicit})
 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];
 
-
+*}
+ML {*
 (** problems **)
 
 store_pbt
  (prep_pbt thy "pbl_bieg" [] e_pblID
  (["Biegelinien"],
-  [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
-   (*("#Where",["0 < l_"]), ...wait for &lt; and handling Arbfix*)
-   ("#Find"  ,["Biegelinie b_"]),
-   ("#Relate",["Randbedingungen rb_"])
+  [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
+   (*("#Where",["0 < l_l"]), ...wait for &lt; and handling Arbfix*)
+   ("#Find"  ,["Biegelinie b_b"]),
+   ("#Relate",["Randbedingungen r_b"])
   ],
   append_rls "e_rls" e_rls [], 
   NONE, 
@@ -114,10 +114,10 @@
 store_pbt 
  (prep_pbt thy "pbl_bieg_mom" [] e_pblID
  (["MomentBestimmte","Biegelinien"],
-  [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
-   (*("#Where",["0 < l_"]), ...wait for &lt; and handling Arbfix*)
-   ("#Find"  ,["Biegelinie b_"]),
-   ("#Relate",["RandbedingungenBiegung rb_","RandbedingungenMoment rm_"])
+  [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
+   (*("#Where",["0 < l_l"]), ...wait for &lt; and handling Arbfix*)
+   ("#Find"  ,["Biegelinie b_b"]),
+   ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
   ],
   append_rls "e_rls" e_rls [], 
   NONE, 
@@ -150,8 +150,8 @@
 store_pbt
  (prep_pbt thy "pbl_bieg_vonq" [] e_pblID
  (["vonBelastungZu","Biegelinien"],
-  [("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),
-   ("#Find"  ,["Funktionen funs___"])],
+  [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
+   ("#Find"  ,["Funktionen funs'''"])],
   append_rls "e_rls" e_rls [], 
   NONE, 
   [["Biegelinien","ausBelastung"]]));
@@ -159,8 +159,8 @@
 store_pbt
  (prep_pbt thy "pbl_bieg_randbed" [] e_pblID
  (["setzeRandbedingungen","Biegelinien"],
-  [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
-   ("#Find"  ,["Gleichungen equs___"])],
+  [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
+   ("#Find"  ,["Gleichungen equs'''"])],
   append_rls "e_rls" e_rls [], 
   NONE, 
   [["Biegelinien","setzeRandbedingungenEin"]]));
@@ -168,28 +168,29 @@
 store_pbt
  (prep_pbt thy "pbl_equ_fromfun" [] e_pblID
  (["makeFunctionTo","equation"],
-  [("#Given" ,["functionEq fun_","substitution sub_"]),
-   ("#Find"  ,["equality equ___"])],
+  [("#Given" ,["functionEq fu_n","substitution su_b"]),
+   ("#Find"  ,["equality equ'''"])],
   append_rls "e_rls" e_rls [], 
   NONE, 
   [["Equation","fromFunction"]]));
 
-
+*}
+ML {*
 (** methods **)
 
 val srls = Rls {id="srls_IntegrierenUnd..", 
 		preconds = [], 
 		rew_ord = ("termlessI",termlessI), 
 		erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
-				  [(*for asm in nth_Cons_ ...*)
+				  [(*for asm in NTH_CONS ...*)
 				   Calc ("op <",eval_equ "#less_"),
-				   (*2nd nth_Cons_ pushes n+-1 into asms*)
+				   (*2nd NTH_CONS pushes n+-1 into asms*)
 				   Calc("op +", eval_binop "#add_")
 				   ], 
 		srls = Erls, calc = [],
-		rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
+		rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
 			 Calc("op +", eval_binop "#add_"),
-			 Thm ("nth_Nil_",num_str @{thm nth_Nil_}),
+			 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
 			 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
 			 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
 			 Calc("Atools.argument'_in",
@@ -202,15 +203,15 @@
 	 preconds = [], 
 	 rew_ord = ("termlessI",termlessI), 
 	 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
-			   [(*for asm in nth_Cons_ ...*)
+			   [(*for asm in NTH_CONS ...*)
 			    Calc ("op <",eval_equ "#less_"),
-			    (*2nd nth_Cons_ pushes n+-1 into asms*)
+			    (*2nd NTH_CONS pushes n+-1 into asms*)
 			    Calc("op +", eval_binop "#add_")
 			    ], 
 	 srls = Erls, calc = [],
-	 rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
+	 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
 		  Calc("op +", eval_binop "#add_"),
-		  Thm ("nth_Nil_", num_str @{thm nth_Nil_}),
+		  Thm ("NTH_NIL", num_str @{thm NTH_NIL}),
 		  Calc("Tools.lhs", eval_lhs "eval_lhs_"),
 		  Calc("Atools.filter'_sameFunId",
 		       eval_filter_sameFunId "Atools.filter'_sameFunId"),
@@ -223,16 +224,18 @@
 		  Thm ("hd_thm", num_str @{thm hd_thm})
 		  ],
 	 scr = EmptyScr};
- 
+*}
+
+ML {*
 store_met
     (prep_met thy "met_biege" [] e_metID
 	      (["IntegrierenUndKonstanteBestimmen"],
-	       [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
+	       [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q",
 			    "FunktionsVariable v_v"]),
-		(*("#Where",["0 < l_"]), ...wait for &lt; and handling Arbfix*)
-		("#Find"  ,["Biegelinie b_"]),
-		("#Relate",["RandbedingungenBiegung rb_",
-			    "RandbedingungenMoment rm_"])
+		(*("#Where",["0 < l_l"]), ...wait for &lt; and handling Arbfix*)
+		("#Find"  ,["Biegelinie b_b"]),
+		("#Relate",["RandbedingungenBiegung r_b",
+			    "RandbedingungenMoment r_m"])
 		],
 	       {rew_ord'="tless_true", 
 		rls' = append_rls "erls_IntegrierenUndK.." e_rls 
@@ -242,74 +245,76 @@
 		calc = [], srls = srls, prls = Erls,
 		crls = Atools_erls, nrls = Erls},
 "Script BiegelinieScript                                                  " ^
-"(l_::real) (q__::real) (v_v::real) (b_::real=>real)                       " ^
-"(rb_::bool list) (rm_::bool list) =                                      " ^
-"  (let q___ = Take (q_ v_v = q__);                                        " ^
-"       q___ = ((Rewrite sym_real_minus_eq_cancel True) @@                " ^
-"              (Rewrite Belastung_Querkraft True)) q___;                  " ^
-"      (Q__:: bool) =                                                     " ^
-"             (SubProblem (Biegelinie_,[named,integrate,function],        " ^
+"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real)                   " ^
+"(r_b::bool list) (r_m::bool list) =                                      " ^
+"  (let q___q = Take (q_q v_v = q__q);                                       " ^
+"       q___q = ((Rewrite sym_real_minus_eq_cancel True) @@                " ^
+"              (Rewrite Belastung_Querkraft True)) q___q;                  " ^
+"      (Q__Q:: bool) =                                                     " ^
+"             (SubProblem (Biegelinie',[named,integrate,function],        " ^
 "                          [diff,integration,named])                      " ^
-"                          [REAL (rhs q___), REAL v_v, real_REAL Q]);   " ^
-"       Q__ = Rewrite Querkraft_Moment True Q__;                          " ^
-"      (M__::bool) =                                                      " ^
-"             (SubProblem (Biegelinie_,[named,integrate,function],        " ^
+"                          [REAL (rhs q___q), REAL v_v, REAL_REAL Q]);   " ^
+"       Q__Q = Rewrite Querkraft_Moment True Q__Q;                          " ^
+"      (M__M::bool) =                                                      " ^
+"             (SubProblem (Biegelinie',[named,integrate,function],        " ^
 "                          [diff,integration,named])                      " ^
-"                          [REAL (rhs Q__), REAL v_v, real_REAL M_b]);  " ^
-"       e1__ = nth_ 1 rm_;                                                " ^
-"      (x1__::real) = argument_in (lhs e1__);                             " ^
-"      (M1__::bool) = (Substitute [v_ = x1__]) M__;                       " ^
-"       M1__        = (Substitute [e1__]) M1__ ;                          " ^
-"       M2__ = Take M__;                                                  " ^
-(*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*)
-"       e2__ = nth_ 2 rm_;                                                " ^
-"      (x2__::real) = argument_in (lhs e2__);                             " ^
-"      (M2__::bool) = ((Substitute [v_ = x2__]) @@                        " ^
-"                      (Substitute [e2__])) M2__;                         " ^
-"      (c_1_2__::bool list) =                                             " ^
-"             (SubProblem (Biegelinie_,[linear,system],[no_met])          " ^
-"                          [booll_ [M1__, M2__], reall [c,c_2]]);         " ^
-"       M__ = Take  M__;                                                  " ^
-"       M__ = ((Substitute c_1_2__) @@                                    " ^
+"                          [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]);  " ^
+"       e__1 = NTH 1 r_m;                                                " ^
+"      (x__1::real) = argument_in (lhs e__1);                             " ^
+"      (M__1::bool) = (Substitute [v_v = x__1]) M__M;                       " ^
+"       M__1        = (Substitute [e__1]) M__1 ;                          " ^
+"       M__2 = Take M__M;                                                  " ^
+(*without this Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
+"       e__2 = NTH 2 r_m;                                                " ^
+"      (x__2::real) = argument_in (lhs e__2);                             " ^
+"      (M__2::bool) = ((Substitute [v_v = x__2]) @@                        " ^
+"                      (Substitute [e__2])) M__2;                         " ^
+"      (c_1_2::bool list) =                                             " ^
+"             (SubProblem (Biegelinie',[linear,system],[no_met])          " ^
+"                          [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]);         " ^
+"       M__M = Take  M__M;                                                  " ^
+"       M__M = ((Substitute c_1_2) @@                                    " ^
 "              (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^
 "                                   simplify_System False)) @@ " ^
 "              (Rewrite Moment_Neigung False) @@ " ^
-"              (Rewrite make_fun_explicit False)) M__;                    " ^
+"              (Rewrite make_fun_explicit False)) M__M;                    " ^
 (*----------------------- and the same once more ------------------------*)
-"      (N__:: bool) =                                                     " ^
-"             (SubProblem (Biegelinie_,[named,integrate,function],        " ^
+"      (N__N:: bool) =                                                     " ^
+"             (SubProblem (Biegelinie',[named,integrate,function],        " ^
 "                          [diff,integration,named])                      " ^
-"                          [REAL (rhs M__), REAL v_v, real_REAL y']);   " ^
-"      (B__:: bool) =                                                     " ^
-"             (SubProblem (Biegelinie_,[named,integrate,function],        " ^
+"                          [REAL (rhs M__M), REAL v_v, REAL_REAL y']);   " ^
+"      (B__B:: bool) =                                                     " ^
+"             (SubProblem (Biegelinie',[named,integrate,function],        " ^
 "                          [diff,integration,named])                      " ^
-"                          [REAL (rhs N__), REAL v_v, real_REAL y]);    " ^
-"       e1__ = nth_ 1 rb_;                                                " ^
-"      (x1__::real) = argument_in (lhs e1__);                             " ^
-"      (B1__::bool) = (Substitute [v_ = x1__]) B__;                       " ^
-"       B1__        = (Substitute [e1__]) B1__ ;                          " ^
-"       B2__ = Take B__;                                                  " ^
-"       e2__ = nth_ 2 rb_;                                                " ^
-"      (x2__::real) = argument_in (lhs e2__);                             " ^
-"      (B2__::bool) = ((Substitute [v_ = x2__]) @@                        " ^
-"                      (Substitute [e2__])) B2__;                         " ^
-"      (c_1_2__::bool list) =                                             " ^
-"             (SubProblem (Biegelinie_,[linear,system],[no_met])          " ^
-"                          [booll_ [B1__, B2__], reall [c,c_2]]);         " ^
-"       B__ = Take  B__;                                                  " ^
-"       B__ = ((Substitute c_1_2__) @@                                    " ^
-"              (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__   " ^
-" in B__)"
+"                          [REAL (rhs N__N), REAL v_v, REAL_REAL y]);    " ^
+"       e__1 = NTH 1 r_b;                                                " ^
+"      (x__1::real) = argument_in (lhs e__1);                             " ^
+"      (B__1::bool) = (Substitute [v_v = x__1]) B__B;                       " ^
+"       B__1        = (Substitute [e__1]) B__1 ;                          " ^
+"       B__2 = Take B__B;                                                  " ^
+"       e__2 = NTH 2 r_b;                                                " ^
+"      (x__2::real) = argument_in (lhs e__2);                             " ^
+"      (B__2::bool) = ((Substitute [v_v = x__2]) @@                        " ^
+"                      (Substitute [e__2])) B__2;                         " ^
+"      (c_1_2::bool list) =                                             " ^
+"             (SubProblem (Biegelinie',[linear,system],[no_met])          " ^
+"                          [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]);         " ^
+"       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)"
 ));
+*}
+ML {*
 
 store_met
     (prep_met thy "met_biege_2" [] e_metID
 	      (["IntegrierenUndKonstanteBestimmen2"],
-	       [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
+	       [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q",
 			    "FunktionsVariable v_v"]),
-		(*("#Where",["0 < l_"]), ...wait for &lt; and handling Arbfix*)
-		("#Find"  ,["Biegelinie b_"]),
-		("#Relate",["Randbedingungen rb_"])
+		(*("#Where",["0 < l_l"]), ...wait for &lt; and handling Arbfix*)
+		("#Find"  ,["Biegelinie b_b"]),
+		("#Relate",["Randbedingungen r_b"])
 		],
 	       {rew_ord'="tless_true", 
 		rls' = append_rls "erls_IntegrierenUndK.." e_rls 
@@ -326,25 +331,27 @@
 				   ],
 		prls = Erls, crls = Atools_erls, nrls = Erls},
 "Script Biegelinie2Script                                                 " ^
-"(l_::real) (q__::real) (v_v::real) (b_::real=>real) (rb_::bool list) =    " ^
+"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
 "  (let                                                                   " ^
-"      (funs_:: bool list) =                                              " ^
-"             (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien],      " ^
+"      (fun_s:: bool list) =                                              " ^
+"             (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien],      " ^
 "                          [Biegelinien,ausBelastung])                    " ^
-"                          [REAL q__, REAL v_]);                        " ^
-"      (equs_::bool list) =                                               " ^
-"             (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien]," ^
+"                          [REAL q__q, REAL v_v]);                        " ^
+"      (equ_s::bool list) =                                               " ^
+"             (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien]," ^
 "                          [Biegelinien,setzeRandbedingungenEin])         " ^
-"                          [booll_ funs_, booll_ rb_]);                   " ^
-"      (cons_::bool list) =                                               " ^
-"             (SubProblem (Biegelinie_,[linear,system],[no_met])          " ^
-"                          [booll_ equs_, reall [c,c_2,c_3,c_4]]);        " ^
-"       B_ = Take (lastI funs_);                                          " ^
-"       B_ = ((Substitute cons_) @@                                       " ^
-"              (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_   " ^
-" in B_)"
+"                          [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)"
 ));
 
+*}
+ML {*
 store_met
     (prep_met thy "met_biege_intconst_2" [] e_metID
 	      (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],
@@ -389,11 +396,13 @@
 "empty_script"
 ));
 
+*}
+ML {*
 store_met
     (prep_met thy "met_biege_ausbelast" [] e_metID
 	      (["Biegelinien","ausBelastung"],
-	       [("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),
-		("#Find"  ,["Funktionen funs_"])],
+	       [("#Given" ,["Streckenlast q__q","FunktionsVariable v_v"]),
+		("#Find"  ,["Funktionen fun_s"])],
 	       {rew_ord'="tless_true", 
 		rls' = append_rls "erls_ausBelastung" e_rls 
 				  [Calc ("Atools.ident",eval_ident "#ident_"),
@@ -403,118 +412,121 @@
 		srls = append_rls "srls_ausBelastung" e_rls 
 				  [Calc("Tools.rhs", eval_rhs"eval_rhs_")], 
 		prls = e_rls, crls = Atools_erls, nrls = e_rls},
-"Script Belastung2BiegelScript (q__::real) (v_v::real) =                   " ^
-"  (let q___ = Take (q_ v_v = q__);                                        " ^
-"       q___ = ((Rewrite sym_real_minus_eq_cancel True) @@                " ^
-"              (Rewrite Belastung_Querkraft True)) q___;                  " ^
-"      (Q__:: bool) =                                                     " ^
-"             (SubProblem (Biegelinie_,[named,integrate,function],        " ^
+"Script Belastung2BiegelScript (q__q::real) (v_v::real) =                   " ^
+"  (let q___q = Take (q_q v_v = q__q);                                        " ^
+"       q___q = ((Rewrite sym_real_minus_eq_cancel True) @@                " ^
+"              (Rewrite Belastung_Querkraft True)) q___q;                  " ^
+"      (Q__Q:: bool) =                                                     " ^
+"             (SubProblem (Biegelinie',[named,integrate,function],        " ^
 "                          [diff,integration,named])                      " ^
-"                          [REAL (rhs q___), REAL v_v, real_REAL Q]);   " ^
-"       M__ = Rewrite Querkraft_Moment True Q__;                          " ^
-"      (M__::bool) =                                                      " ^
-"             (SubProblem (Biegelinie_,[named,integrate,function],        " ^
+"                          [REAL (rhs q___q), REAL v_v, REAL_REAL Q]);   " ^
+"       M__M = Rewrite Querkraft_Moment True Q__Q;                          " ^
+"      (M__M::bool) =                                                      " ^
+"             (SubProblem (Biegelinie',[named,integrate,function],        " ^
 "                          [diff,integration,named])                      " ^
-"                          [REAL (rhs M__), REAL v_v, real_REAL M_b]);  " ^
-"       N__ = ((Rewrite Moment_Neigung False) @@                          " ^
-"              (Rewrite make_fun_explicit False)) M__;                    " ^
-"      (N__:: bool) =                                                     " ^
-"             (SubProblem (Biegelinie_,[named,integrate,function],        " ^
+"                          [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]);  " ^
+"       N__N = ((Rewrite Moment_Neigung False) @@                          " ^
+"              (Rewrite make_fun_explicit False)) M__M;                    " ^
+"      (N__N:: bool) =                                                     " ^
+"             (SubProblem (Biegelinie',[named,integrate,function],        " ^
 "                          [diff,integration,named])                      " ^
-"                          [REAL (rhs N__), REAL v_v, real_REAL y']);   " ^
-"      (B__:: bool) =                                                     " ^
-"             (SubProblem (Biegelinie_,[named,integrate,function],        " ^
+"                          [REAL (rhs N__N), REAL v_v, REAL_REAL y']);   " ^
+"      (B__B:: bool) =                                                     " ^
+"             (SubProblem (Biegelinie',[named,integrate,function],        " ^
 "                          [diff,integration,named])                      " ^
-"                          [REAL (rhs N__), REAL v_v, real_REAL y])     " ^
-" in [Q__, M__, N__, B__])"
+"                          [REAL (rhs N__N), REAL v_v, REAL_REAL y])     " ^
+" in [Q__Q, M__M, N__N, B__B])"
 ));
 
+*}
+ML {*
 store_met
     (prep_met thy "met_biege_setzrand" [] e_metID
 	      (["Biegelinien","setzeRandbedingungenEin"],
-	       [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
-		("#Find"  ,["Gleichungen equs___"])],
+	       [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
+		("#Find"  ,["Gleichungen equs'''"])],
 	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
 		srls = srls2, 
 		prls=e_rls,
 	     crls = Atools_erls, nrls = e_rls},
-"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^
-" (let b1_ = nth_ 1 rb_;                                         " ^
-"      fs_ = filter_sameFunId (lhs b1_) funs_;                   " ^
-"      (e1_::bool) =                                             " ^
-"             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
+"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
+" (let b_1 = NTH 1 r_b;                                         " ^
+"      f_s = filter_sameFunId (lhs b_1) fun_s;                   " ^
+"      (e_1::bool) =                                             " ^
+"             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
 "                          [Equation,fromFunction])              " ^
-"                          [BOOL (hd fs_), BOOL b1_]);         " ^
-"      b2_ = nth_ 2 rb_;                                         " ^
-"      fs_ = filter_sameFunId (lhs b2_) funs_;                   " ^
-"      (e2_::bool) =                                             " ^
-"             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
+"                          [BOOL (hd f_s), BOOL b_1]);         " ^
+"      b_2 = NTH 2 r_b;                                         " ^
+"      f_s = filter_sameFunId (lhs b_2) fun_s;                   " ^
+"      (e_2::bool) =                                             " ^
+"             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
 "                          [Equation,fromFunction])              " ^
-"                          [BOOL (hd fs_), BOOL b2_]);         " ^
-"      b3_ = nth_ 3 rb_;                                         " ^
-"      fs_ = filter_sameFunId (lhs b3_) funs_;                   " ^
-"      (e3_::bool) =                                             " ^
-"             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
+"                          [BOOL (hd f_s), BOOL b_2]);         " ^
+"      b_3 = NTH 3 r_b;                                         " ^
+"      f_s = filter_sameFunId (lhs b_3) fun_s;                   " ^
+"      (e_3::bool) =                                             " ^
+"             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
 "                          [Equation,fromFunction])              " ^
-"                          [BOOL (hd fs_), BOOL b3_]);         " ^
-"      b4_ = nth_ 4 rb_;                                         " ^
-"      fs_ = filter_sameFunId (lhs b4_) funs_;                   " ^
-"      (e4_::bool) =                                             " ^
-"             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
+"                          [BOOL (hd f_s), BOOL b_3]);         " ^
+"      b_4 = NTH 4 r_b;                                         " ^
+"      f_s = filter_sameFunId (lhs b_4) fun_s;                   " ^
+"      (e_4::bool) =                                             " ^
+"             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
 "                          [Equation,fromFunction])              " ^
-"                          [BOOL (hd fs_), BOOL b4_])          " ^
-" in [e1_,e2_,e3_,e4_])"
+"                          [BOOL (hd f_s), BOOL b_4])          " ^
+" in [e_1,e_2,e_3,e_4])"
 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^
-" (let b1_ = nth_ 1 rb_;                                         " ^
-"      fs_ = filter (sameFunId (lhs b1_)) funs_;                 " ^
-"      (e1_::bool) =                                             " ^
-"             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
+"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
+" (let b_1 = NTH 1 r_b;                                         " ^
+"      f_s = filter (sameFunId (lhs b_1)) fun_s;                 " ^
+"      (e_1::bool) =                                             " ^
+"             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
 "                          [Equation,fromFunction])              " ^
-"                          [BOOL (hd fs_), BOOL b1_]);         " ^
-"      b2_ = nth_ 2 rb_;                                         " ^
-"      fs_ = filter (sameFunId (lhs b2_)) funs_;                 " ^
-"      (e2_::bool) =                                             " ^
-"             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
+"                          [BOOL (hd f_s), BOOL b_1]);         " ^
+"      b_2 = NTH 2 r_b;                                         " ^
+"      f_s = filter (sameFunId (lhs b_2)) fun_s;                 " ^
+"      (e_2::bool) =                                             " ^
+"             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
 "                          [Equation,fromFunction])              " ^
-"                          [BOOL (hd fs_), BOOL b2_]);         " ^
-"      b3_ = nth_ 3 rb_;                                         " ^
-"      fs_ = filter (sameFunId (lhs b3_)) funs_;                 " ^
-"      (e3_::bool) =                                             " ^
-"             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
+"                          [BOOL (hd f_s), BOOL b_2]);         " ^
+"      b_3 = NTH 3 r_b;                                         " ^
+"      f_s = filter (sameFunId (lhs b_3)) fun_s;                 " ^
+"      (e_3::bool) =                                             " ^
+"             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
 "                          [Equation,fromFunction])              " ^
-"                          [BOOL (hd fs_), BOOL b3_]);         " ^
-"      b4_ = nth_ 4 rb_;                                         " ^
-"      fs_ = filter (sameFunId (lhs b4_)) funs_;                 " ^
-"      (e4_::bool) =                                             " ^
-"             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
+"                          [BOOL (hd f_s), BOOL b_3]);         " ^
+"      b_4 = NTH 4 r_b;                                         " ^
+"      f_s = filter (sameFunId (lhs b_4)) fun_s;                 " ^
+"      (e_4::bool) =                                             " ^
+"             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
 "                          [Equation,fromFunction])              " ^
-"                          [BOOL (hd fs_), BOOL b4_])          " ^
-" in [e1_,e2_,e3_,e4_])"*)
+"                          [BOOL (hd f_s), BOOL b_4])          " ^
+" in [e_1,e_2,e_3,e_4])"*)
 ));
 
+*}
+ML {*
 store_met
     (prep_met thy "met_equ_fromfun" [] e_metID
 	      (["Equation","fromFunction"],
-	       [("#Given" ,["functionEq fun_","substitution sub_"]),
-		("#Find"  ,["equality equ___"])],
+	       [("#Given" ,["functionEq fu_n","substitution su_b"]),
+		("#Find"  ,["equality equ'''"])],
 	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
 		srls = append_rls "srls_in_EquationfromFunc" e_rls
 				  [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
 				   Calc("Atools.argument'_in",
 					eval_argument_in
 					    "Atools.argument'_in")], 
-		prls=e_rls,
-	     crls = Atools_erls, nrls = e_rls},
+		prls=e_rls, crls = Atools_erls, nrls = e_rls},
 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
        0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
-"Script Function2Equality (fun_::bool) (sub_::bool) =" ^
-" (let fun_ = Take fun_;                             " ^
-"      bdv_ = argument_in (lhs fun_);                " ^
-"      val_ = argument_in (lhs sub_);                " ^
-"      equ_ = (Substitute [bdv_ = val_]) fun_;       " ^
-"      equ_ = (Substitute [sub_]) fun_               " ^
-" in (Rewrite_Set norm_Rational False) equ_)             "
+"Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
+" (let fu_n = Take fu_n;                             " ^
+"      bd_v = argument_in (lhs fu_n);                " ^
+"      va_l = argument_in (lhs su_b);                " ^
+"      eq_u = (Substitute [bd_v = va_l]) fu_n;       " ^
+"      eq_u = (Substitute [su_b]) fu_n               " ^
+" in (Rewrite_Set norm_Rational False) eq_u)             "
 ));
 *}
 




