1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Thu Mar 08 14:33:34 2012 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Sat Mar 10 09:41:09 2012 +0100
1.3 @@ -228,125 +228,123 @@
1.4
1.5 ML {*
1.6 store_met
1.7 - (prep_met thy "met_biege" [] e_metID
1.8 - (["IntegrierenUndKonstanteBestimmen"],
1.9 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q",
1.10 - "FunktionsVariable v_v"]),
1.11 + (prep_met thy "met_biege" [] e_metID
1.12 + (["IntegrierenUndKonstanteBestimmen"],
1.13 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
1.14 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.15 - ("#Find" ,["Biegelinie b_b"]),
1.16 - ("#Relate",["RandbedingungenBiegung r_b",
1.17 - "RandbedingungenMoment r_m"])
1.18 - ],
1.19 - {rew_ord'="tless_true",
1.20 - rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.21 - [Calc ("Atools.ident",eval_ident "#ident_"),
1.22 - Thm ("not_true",num_str @{thm not_true}),
1.23 - Thm ("not_false",num_str @{thm not_false})],
1.24 - calc = [], srls = srls, prls = Erls,
1.25 - crls = Atools_erls, nrls = Erls},
1.26 -"Script BiegelinieScript " ^
1.27 -"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
1.28 -"(r_b::bool list) (r_m::bool list) = " ^
1.29 -" (let q___q = Take (q_q v_v = q__q); " ^
1.30 -" q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
1.31 -" (Rewrite Belastung_Querkraft True)) q___q; " ^
1.32 -" (Q__Q:: bool) = " ^
1.33 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.34 -" [diff,integration,named]) " ^
1.35 + ("#Find" ,["Biegelinie b_b"]),
1.36 + ("#Relate",["RandbedingungenBiegung r_b", "RandbedingungenMoment r_m"])],
1.37 + {rew_ord'="tless_true",
1.38 + rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.39 + [Calc ("Atools.ident",eval_ident "#ident_"),
1.40 + Thm ("not_true",num_str @{thm not_true}),
1.41 + Thm ("not_false",num_str @{thm not_false})],
1.42 + calc = [], srls = srls, prls = Erls, crls = Atools_erls, nrls = Erls},
1.43 +"Script BiegelinieScript " ^
1.44 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
1.45 +"(r_b::bool list) (r_m::bool list) = " ^
1.46 +" (let q___q = Take (qq v_v = q__q); " ^
1.47 +" q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
1.48 +" (Rewrite Belastung_Querkraft True)) q___q; " ^
1.49 +" (Q__Q:: bool) = " ^
1.50 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.51 +" [diff,integration,named]) " ^
1.52 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
1.53 -" Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
1.54 -" (M__M::bool) = " ^
1.55 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.56 -" [diff,integration,named]) " ^
1.57 +" Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
1.58 +" (M__M::bool) = " ^
1.59 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.60 +" [diff,integration,named]) " ^
1.61 " [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^
1.62 + (*([5], Res), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
1.63 " e__1 = NTH 1 r_m; " ^
1.64 -" (x__1::real) = argument_in (lhs e__1); " ^
1.65 -" (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
1.66 -" M__1 = (Substitute [e__1]) M__1 ; " ^
1.67 -" M__2 = Take M__M; " ^
1.68 -(*without this Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
1.69 +" (x__1::real) = argument_in (lhs e__1); " ^
1.70 +" (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
1.71 + (*([6], Res), M_b 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
1.72 +" M__1 = (Substitute [e__1]) M__1; " ^
1.73 + (*([7], Res), 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
1.74 +" M__2 = Take M__M; " ^
1.75 + (*([8], Frm), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
1.76 +(*without above Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
1.77 " e__2 = NTH 2 r_m; " ^
1.78 -" (x__2::real) = argument_in (lhs e__2); " ^
1.79 -" (M__2::bool) = ((Substitute [v_v = x__2]) @@ " ^
1.80 -" (Substitute [e__2])) M__2; " ^
1.81 -" (c_1_2::bool list) = " ^
1.82 -" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
1.83 -" [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
1.84 -" M__M = Take M__M; " ^
1.85 +" (x__2::real) = argument_in (lhs e__2); " ^
1.86 +" (M__2::bool) = (Substitute [v_v = x__2]) M__M; " ^
1.87 + (*([8], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
1.88 +" M__2 = (Substitute [e__2]) M__2; " ^
1.89 + (**)
1.90 +" (c_1_2::bool list) = " ^
1.91 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
1.92 +" [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
1.93 +" M__M = Take M__M; " ^
1.94 " M__M = ((Substitute c_1_2) @@ " ^
1.95 -" (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^
1.96 -" simplify_System False)) @@ " ^
1.97 -" (Rewrite Moment_Neigung False) @@ " ^
1.98 -" (Rewrite make_fun_explicit False)) M__M; " ^
1.99 +" (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)] " ^
1.100 +" simplify_System False)) @@ " ^
1.101 +" (Rewrite Moment_Neigung False) @@ " ^
1.102 +" (Rewrite make_fun_explicit False)) M__M; " ^
1.103 (*----------------------- and the same once more ------------------------*)
1.104 -" (N__N:: bool) = " ^
1.105 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.106 -" [diff,integration,named]) " ^
1.107 +" (N__N:: bool) = " ^
1.108 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.109 +" [diff,integration,named]) " ^
1.110 " [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^
1.111 -" (B__B:: bool) = " ^
1.112 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.113 -" [diff,integration,named]) " ^
1.114 +" (B__B:: bool) = " ^
1.115 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.116 +" [diff,integration,named]) " ^
1.117 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^
1.118 " e__1 = NTH 1 r_b; " ^
1.119 -" (x__1::real) = argument_in (lhs e__1); " ^
1.120 -" (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
1.121 -" B__1 = (Substitute [e__1]) B__1 ; " ^
1.122 -" B__2 = Take B__B; " ^
1.123 +" (x__1::real) = argument_in (lhs e__1); " ^
1.124 +" (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
1.125 +" B__1 = (Substitute [e__1]) B__1 ; " ^
1.126 +" B__2 = Take B__B; " ^
1.127 " e__2 = NTH 2 r_b; " ^
1.128 -" (x__2::real) = argument_in (lhs e__2); " ^
1.129 -" (B__2::bool) = ((Substitute [v_v = x__2]) @@ " ^
1.130 -" (Substitute [e__2])) B__2; " ^
1.131 -" (c_1_2::bool list) = " ^
1.132 -" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
1.133 -" [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
1.134 -" B__B = Take B__B; " ^
1.135 +" (x__2::real) = argument_in (lhs e__2); " ^
1.136 +" (B__2::bool) = (Substitute [v_v = x__2]) B__B; " ^
1.137 +" B__2 = (Substitute [e__2]) B__2 ; " ^
1.138 +" (c_1_2::bool list) = " ^
1.139 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
1.140 +" [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
1.141 +" B__B = Take B__B; " ^
1.142 " B__B = ((Substitute c_1_2) @@ " ^
1.143 -" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
1.144 +" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
1.145 " in B__B)"
1.146 ));
1.147 *}
1.148 ML {*
1.149 -
1.150 store_met
1.151 - (prep_met thy "met_biege_2" [] e_metID
1.152 - (["IntegrierenUndKonstanteBestimmen2"],
1.153 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q",
1.154 - "FunktionsVariable v_v"]),
1.155 + (prep_met thy "met_biege_2" [] e_metID
1.156 + (["IntegrierenUndKonstanteBestimmen2"],
1.157 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
1.158 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.159 - ("#Find" ,["Biegelinie b_b"]),
1.160 - ("#Relate",["Randbedingungen r_b"])
1.161 - ],
1.162 - {rew_ord'="tless_true",
1.163 - rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.164 - [Calc ("Atools.ident",eval_ident "#ident_"),
1.165 - Thm ("not_true",num_str @{thm not_true}),
1.166 - Thm ("not_false",num_str @{thm not_false})],
1.167 - calc = [],
1.168 - srls = append_rls "erls_IntegrierenUndK.." e_rls
1.169 - [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.170 - Calc ("Atools.ident",eval_ident "#ident_"),
1.171 - Thm ("last_thmI",num_str @{thm last_thmI}),
1.172 - Thm ("if_True",num_str @{thm if_True}),
1.173 - Thm ("if_False",num_str @{thm if_False})
1.174 - ],
1.175 - prls = Erls, crls = Atools_erls, nrls = Erls},
1.176 -"Script Biegelinie2Script " ^
1.177 + ("#Find" ,["Biegelinie b_b"]),
1.178 + ("#Relate",["Randbedingungen r_b"])],
1.179 + {rew_ord'="tless_true",
1.180 + rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.181 + [Calc ("Atools.ident",eval_ident "#ident_"),
1.182 + Thm ("not_true",num_str @{thm not_true}),
1.183 + Thm ("not_false",num_str @{thm not_false})],
1.184 + calc = [],
1.185 + srls = append_rls "erls_IntegrierenUndK.." e_rls
1.186 + [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.187 + Calc ("Atools.ident",eval_ident "#ident_"),
1.188 + Thm ("last_thmI",num_str @{thm last_thmI}),
1.189 + Thm ("if_True",num_str @{thm if_True}),
1.190 + Thm ("if_False",num_str @{thm if_False})],
1.191 + prls = Erls, crls = Atools_erls, nrls = Erls},
1.192 +"Script Biegelinie2Script " ^
1.193 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
1.194 -" (let " ^
1.195 -" (fun_s:: bool list) = " ^
1.196 -" (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
1.197 -" [Biegelinien,ausBelastung]) " ^
1.198 -" [REAL q__q, REAL v_v]); " ^
1.199 -" (equ_s::bool list) = " ^
1.200 -" (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien]," ^
1.201 -" [Biegelinien,setzeRandbedingungenEin]) " ^
1.202 +" (let " ^
1.203 +" (fun_s:: bool list) = " ^
1.204 +" (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
1.205 +" [Biegelinien,ausBelastung]) " ^
1.206 +" [REAL q__q, REAL v_v]); " ^
1.207 +" (equ_s::bool list) = " ^
1.208 +" (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien], " ^
1.209 +" [Biegelinien,setzeRandbedingungenEin]) " ^
1.210 " [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^
1.211 -" (con_s::bool list) = " ^
1.212 -" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
1.213 -" [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
1.214 +" (con_s::bool list) = " ^
1.215 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
1.216 +" [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
1.217 " B_B = Take (lastI fun_s); " ^
1.218 " B_B = ((Substitute con_s) @@ " ^
1.219 -" (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
1.220 +" (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
1.221 " in B_B)"
1.222 ));
1.223
1.224 @@ -399,42 +397,42 @@
1.225 *}
1.226 ML {*
1.227 store_met
1.228 - (prep_met thy "met_biege_ausbelast" [] e_metID
1.229 - (["Biegelinien","ausBelastung"],
1.230 - [("#Given" ,["Streckenlast q__q","FunktionsVariable v_v"]),
1.231 - ("#Find" ,["Funktionen fun_s"])],
1.232 - {rew_ord'="tless_true",
1.233 - rls' = append_rls "erls_ausBelastung" e_rls
1.234 - [Calc ("Atools.ident",eval_ident "#ident_"),
1.235 - Thm ("not_true",num_str @{thm not_true}),
1.236 - Thm ("not_false",num_str @{thm not_false})],
1.237 - calc = [],
1.238 - srls = append_rls "srls_ausBelastung" e_rls
1.239 - [Calc("Tools.rhs", eval_rhs"eval_rhs_")],
1.240 - prls = e_rls, crls = Atools_erls, nrls = e_rls},
1.241 -"Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
1.242 -" (let q___q = Take (q_q v_v = q__q); " ^
1.243 -" q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
1.244 -" (Rewrite Belastung_Querkraft True)) q___q; " ^
1.245 -" (Q__Q:: bool) = " ^
1.246 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.247 -" [diff,integration,named]) " ^
1.248 -" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
1.249 -" M__M = Rewrite Querkraft_Moment True Q__Q; " ^
1.250 -" (M__M::bool) = " ^
1.251 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.252 -" [diff,integration,named]) " ^
1.253 -" [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
1.254 -" N__N = ((Rewrite Moment_Neigung False) @@ " ^
1.255 -" (Rewrite make_fun_explicit False)) M__M; " ^
1.256 -" (N__N:: bool) = " ^
1.257 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.258 -" [diff,integration,named]) " ^
1.259 -" [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
1.260 -" (B__B:: bool) = " ^
1.261 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.262 -" [diff,integration,named]) " ^
1.263 -" [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
1.264 + (prep_met thy "met_biege_ausbelast" [] e_metID
1.265 + (["Biegelinien", "ausBelastung"],
1.266 + [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
1.267 + ("#Find" ,["Funktionen fun_s"])],
1.268 + {rew_ord'="tless_true",
1.269 + rls' = append_rls "erls_ausBelastung" e_rls
1.270 + [Calc ("Atools.ident", eval_ident "#ident_"),
1.271 + Thm ("not_true", num_str @{thm not_true}),
1.272 + Thm ("not_false", num_str @{thm not_false})],
1.273 + calc = [],
1.274 + srls = append_rls "srls_ausBelastung" e_rls
1.275 + [Calc ("Tools.rhs", eval_rhs "eval_rhs_")],
1.276 + prls = e_rls, crls = Atools_erls, nrls = e_rls},
1.277 +"Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
1.278 +" (let q___q = Take (qq v_v = q__q); " ^
1.279 +" q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
1.280 +" (Rewrite Belastung_Querkraft True)) q___q; " ^
1.281 +" (Q__Q:: bool) = " ^
1.282 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.283 +" [diff,integration,named]) " ^
1.284 +" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
1.285 +" M__M = Rewrite Querkraft_Moment True Q__Q; " ^
1.286 +" (M__M::bool) = " ^
1.287 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.288 +" [diff,integration,named]) " ^
1.289 +" [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
1.290 +" N__N = ((Rewrite Moment_Neigung False) @@ " ^
1.291 +" (Rewrite make_fun_explicit False)) M__M; " ^
1.292 +" (N__N:: bool) = " ^
1.293 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.294 +" [diff,integration,named]) " ^
1.295 +" [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
1.296 +" (B__B:: bool) = " ^
1.297 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.298 +" [diff,integration,named]) " ^
1.299 +" [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
1.300 " in [Q__Q, M__M, N__N, B__B])"
1.301 ));
1.302
1.303 @@ -442,9 +440,9 @@
1.304 ML {*
1.305 store_met
1.306 (prep_met thy "met_biege_setzrand" [] e_metID
1.307 - (["Biegelinien","setzeRandbedingungenEin"],
1.308 - [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
1.309 - ("#Find" ,["Gleichungen equs'''"])],
1.310 + (["Biegelinien", "setzeRandbedingungenEin"],
1.311 + [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
1.312 + ("#Find" , ["Gleichungen equs'''"])],
1.313 {rew_ord'="tless_true", rls'=Erls, calc = [],
1.314 srls = srls2,
1.315 prls=e_rls,
1.316 @@ -474,7 +472,7 @@
1.317 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.318 " [Equation,fromFunction]) " ^
1.319 " [BOOL (hd f_s), BOOL b_4]) " ^
1.320 -" in [e_1,e_2,e_3,e_4])"
1.321 +" in [e_1, e_2, e_3, e_4])"
1.322 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
1.323 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
1.324 " (let b_1 = NTH 1 r_b; " ^
1.325 @@ -507,17 +505,15 @@
1.326 *}
1.327 ML {*
1.328 store_met
1.329 - (prep_met thy "met_equ_fromfun" [] e_metID
1.330 - (["Equation","fromFunction"],
1.331 - [("#Given" ,["functionEq fu_n","substitution su_b"]),
1.332 - ("#Find" ,["equality equ'''"])],
1.333 - {rew_ord'="tless_true", rls'=Erls, calc = [],
1.334 - srls = append_rls "srls_in_EquationfromFunc" e_rls
1.335 - [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.336 - Calc("Atools.argument'_in",
1.337 - eval_argument_in
1.338 - "Atools.argument'_in")],
1.339 - prls=e_rls, crls = Atools_erls, nrls = e_rls},
1.340 + (prep_met thy "met_equ_fromfun" [] e_metID
1.341 + (["Equation","fromFunction"],
1.342 + [("#Given" ,["functionEq fu_n","substitution su_b"]),
1.343 + ("#Find" ,["equality equ'''"])],
1.344 + {rew_ord'="tless_true", rls'=Erls, calc = [],
1.345 + srls = append_rls "srls_in_EquationfromFunc" e_rls
1.346 + [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.347 + Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")],
1.348 + prls=e_rls, crls = Atools_erls, nrls = e_rls},
1.349 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
1.350 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
1.351 "Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
1.352 @@ -525,8 +521,9 @@
1.353 " bd_v = argument_in (lhs fu_n); " ^
1.354 " va_l = argument_in (lhs su_b); " ^
1.355 " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
1.356 -" eq_u = (Substitute [su_b]) fu_n " ^
1.357 -" in (Rewrite_Set norm_Rational False) eq_u) "
1.358 + (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
1.359 +" eq_u = (Substitute [su_b]) eq_u " ^
1.360 +" in (Rewrite_Set norm_Rational False) eq_u) "
1.361 ));
1.362 *}
1.363