1.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -39,37 +39,37 @@
1.4 val t = str2term"0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
1.5
1.6 if occur_exactly_in [str2term"c", str2term"c_2"] all t
1.7 -then () else raise error "eqsystem.sml occur_exactly_in 1";
1.8 +then () else error "eqsystem.sml occur_exactly_in 1";
1.9
1.10 if not (occur_exactly_in [str2term"c", str2term"c_2", str2term"c_3"] all t)
1.11 -then () else raise error "eqsystem.sml occur_exactly_in 2";
1.12 +then () else error "eqsystem.sml occur_exactly_in 2";
1.13
1.14 if not (occur_exactly_in [str2term"c_2"] all t)
1.15 -then () else raise error "eqsystem.sml occur_exactly_in 3";
1.16 +then () else error "eqsystem.sml occur_exactly_in 3";
1.17
1.18
1.19 val t = str2term"[c,c_2] from_ [c,c_2,c_3] occur_exactly_in \
1.20 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
1.21 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
1.22 if str = "[c, c_2] from_ [c, c_2,\n c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = True" then ()
1.23 -else raise error "eval_occur_exactly_in [c, c_2]";
1.24 +else error "eval_occur_exactly_in [c, c_2]";
1.25
1.26 val t = str2term"[c,c_2,c_3] from_ [c,c_2,c_3] occur_exactly_in \
1.27 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
1.28 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
1.29 if str = "[c, c_2,\n c_3] from_ [c, c_2,\n c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
1.30 -else raise error "eval_occur_exactly_in [c, c_2, c_3]";
1.31 +else error "eval_occur_exactly_in [c, c_2, c_3]";
1.32
1.33 val t = str2term"[c_2] from_ [c,c_2,c_3] occur_exactly_in \
1.34 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
1.35 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
1.36 if str = "[c_2] from_ [c, c_2,\n c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
1.37 -else raise error "eval_occur_exactly_in [c, c_2, c_3]";
1.38 +else error "eval_occur_exactly_in [c, c_2, c_3]";
1.39
1.40 val t = str2term"[] from_ [c,c_2,c_3] occur_exactly_in 0";
1.41 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
1.42 if str = "[] from_ [c, c_2, c_3] occur_exactly_in 0 = True" then ()
1.43 -else raise error "eval_occur_exactly_in [c, c_2, c_3]";
1.44 +else error "eval_occur_exactly_in [c, c_2, c_3]";
1.45
1.46 val t =
1.47 str2term
1.48 @@ -77,7 +77,7 @@
1.49 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
1.50 if str = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in \
1.51 \-1 * (q_0 * L ^^^ 2) / 2 = True" then ()
1.52 -else raise error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
1.53 +else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
1.54
1.55
1.56 "----------- problems --------------------------------------------";
1.57 @@ -93,7 +93,7 @@
1.58 ];
1.59 val SOME (t',_) = rewrite_set_ thy false testrls t;
1.60 if term2str t' = "True" then ()
1.61 -else raise error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
1.62 +else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
1.63
1.64 val SOME t = parse EqSystem.thy "solution L";
1.65 atomty (term_of t);
1.66 @@ -118,7 +118,7 @@
1.67 "#eval_occur_exactly_in_")
1.68 ]) t;
1.69 if t = HOLogic.true_const then ()
1.70 -else raise error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
1.71 +else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
1.72
1.73
1.74 "----------- rewrite-order ord_simplify_System -------------------";
1.75 @@ -128,28 +128,28 @@
1.76 "--- add_commute ---";
1.77 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",
1.78 str2term"c * x") then ()
1.79 -else raise error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c * x) not#1";
1.80 +else error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c * x) not#1";
1.81
1.82 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",
1.83 str2term"c_2") then ()
1.84 -else raise error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c_2) not#2";
1.85 +else error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c_2) not#2";
1.86
1.87 if ord_simplify_System false thy [] (str2term"c * x",
1.88 str2term"c_2") then ()
1.89 -else raise error "integrate.sml, (c * x) < (c_2) not#3";
1.90 +else error "integrate.sml, (c * x) < (c_2) not#3";
1.91
1.92 "--- mult_commute ---";
1.93 if ord_simplify_System false thy [] (str2term"x * c",
1.94 str2term"c * x") then ()
1.95 -else raise error "integrate.sml, (x * c) < (c * x) not#4";
1.96 +else error "integrate.sml, (x * c) < (c * x) not#4";
1.97
1.98 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c",
1.99 str2term"-1 * q_0 * c * (x ^^^ 2 / 2)")
1.100 -then () else raise error "integrate.sml, (. * .) < (. * .) not#5";
1.101 +then () else error "integrate.sml, (. * .) < (. * .) not#5";
1.102
1.103 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c",
1.104 str2term"c * -1 * q_0 * (x ^^^ 2 / 2)")
1.105 -then () else raise error "integrate.sml, (. * .) < (. * .) not#6";
1.106 +then () else error "integrate.sml, (. * .) < (. * .) not#6";
1.107
1.108
1.109 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";
1.110 @@ -161,19 +161,19 @@
1.111 (str2term"bdv_2",str2term"c_2")];
1.112 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
1.113 if term2str t = "[0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2), 0 = c_2]"
1.114 -then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
1.115 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
1.116
1.117 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
1.118 if term2str t = "[L * c + c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2), c_2 = 0]"
1.119 -then () else raise error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
1.120 +then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
1.121
1.122 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
1.123 if term2str t = "[L * c + c_2 = q_0 * L ^^^ 2 / 2, c_2 = 0]"
1.124 -then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
1.125 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
1.126
1.127 val SOME (t,_) = rewrite_set_ thy true order_system t;
1.128 if term2str t = "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"
1.129 -then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
1.130 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
1.131
1.132
1.133 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
1.134 @@ -187,23 +187,23 @@
1.135 \ -1 * q_0 / 24 * L ^^^ 4)]";
1.136 val SOME (t,_) = rewrite_set_ thy true norm_Rational t;
1.137 if term2str t="[0 = c_2, 0 = c_2 + L * c + L ^^^ 4 * q_0 / (EI * 24)]"
1.138 -then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
1.139 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
1.140
1.141 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
1.142 if term2str t = "[0 = c_2, 0 = q_0 * L ^^^ 4 / (24 * EI) + (L * c + c_2)]"
1.143 -then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
1.144 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
1.145
1.146 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
1.147 if term2str t = "[c_2 = 0, L * c + c_2 = 0 + -1 * (q_0 * L ^^^ 4 / (24 * EI))]"
1.148 -then () else raise error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
1.149 +then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
1.150
1.151 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
1.152 if term2str t = "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
1.153 -then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
1.154 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
1.155
1.156 val xxx = rewrite_set_ thy true order_system t;
1.157 if is_none xxx
1.158 -then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
1.159 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
1.160
1.161
1.162 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
1.163 @@ -215,27 +215,27 @@
1.164 (str2term"bdv_2",str2term"c_2")];
1.165 val SOME (e2__,_) = rewrite_terms_ thy dummy_ord Erls [e1__] e2__;
1.166 if term2str e2__ = "L * c + 77 = q_0 * L ^^^ 2 / 2" then ()
1.167 -else raise error "eqsystem.sml top_down_substitution,2x2] subst";
1.168 +else error "eqsystem.sml top_down_substitution,2x2] subst";
1.169
1.170 val SOME (e2__,_) =
1.171 rewrite_set_inst_ thy true bdvs simplify_System_parenthesized e2__;
1.172 if term2str e2__ = "77 + L * c = q_0 * L ^^^ 2 / 2" then ()
1.173 -else raise error "eqsystem.sml top_down_substitution,2x2] simpl_par";
1.174 +else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
1.175
1.176 val SOME (e2__,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs e2__;
1.177 if term2str e2__ = "c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L" then ()
1.178 -else raise error "eqsystem.sml top_down_substitution,2x2] isolate";
1.179 +else error "eqsystem.sml top_down_substitution,2x2] isolate";
1.180
1.181 val t = str2term "[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]";
1.182 val SOME (t,_) = rewrite_set_ thy true order_system t;
1.183 if term2str t = "[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]" then ()
1.184 -else raise error "eqsystem.sml top_down_substitution,2x2] order_system";
1.185 +else error "eqsystem.sml top_down_substitution,2x2] order_system";
1.186
1.187 if not (ord_simplify_System
1.188 false thy []
1.189 (str2term"[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]",
1.190 str2term"[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]"))
1.191 -then () else raise error "eqsystem.sml, order_result rew_ord";
1.192 +then () else error "eqsystem.sml, order_result rew_ord";
1.193
1.194 trace_rewrite:=true;
1.195 trace_rewrite:=false;
1.196 @@ -257,27 +257,27 @@
1.197 rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
1.198 if term2str t = "[0 = c_4, 0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c_3 + c_4),\n\
1.199 \ c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
1.200 -then () else raise error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
1.201 +then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
1.202
1.203 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
1.204 if term2str t = "[c_4 = 0, \
1.205 \L * c_3 + c_4 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2),\n \
1.206 \c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
1.207 -then () else raise error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
1.208 +then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
1.209
1.210 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
1.211 if term2str t = "[c_4 = 0,\
1.212 \ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\
1.213 \ c + (c_2 + (c_3 + c_4)) = 0,\n\
1.214 \ c_2 + (c_3 + c_4) = 0]"
1.215 -then () else raise error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
1.216 +then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
1.217
1.218 val SOME (t,_) = rewrite_set_ thy true order_system t;
1.219 if term2str t = "[c_4 = 0,\
1.220 \ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\
1.221 \ c_2 + (c_3 + c_4) = 0,\n\
1.222 \ c + (c_2 + (c_3 + c_4)) = 0]"
1.223 -then () else raise error "eqsystem.sml rewrite in 4x4 order_system";
1.224 +then () else error "eqsystem.sml rewrite in 4x4 order_system";
1.225
1.226
1.227 "----------- script [EqSystem,normalize,2x2] ---------------------";
1.228 @@ -678,7 +678,7 @@
1.229 Correct "solveForVars [c, c_2]"],
1.230 Where = [],
1.231 Relate = []})] => ()
1.232 - | _ => raise error "eqsystem.sml refine ['normalize','2x2'...]";
1.233 + | _ => error "eqsystem.sml refine ['normalize','2x2'...]";
1.234
1.235
1.236 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
1.237 @@ -699,7 +699,7 @@
1.238 Correct
1.239 "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"],
1.240 Relate = []})] => ()
1.241 - | _ => raise error "eqsystem.sml refine ['triangular','2x2'...]";
1.242 + | _ => error "eqsystem.sml refine ['triangular','2x2'...]";
1.243
1.244
1.245 (*WN051014----------------------------------------------------------------
1.246 @@ -747,7 +747,7 @@
1.247 Matches (["4x4", "linear", "system"], _),
1.248 NoMatch (["triangular", "4x4", "linear", "system"], _),
1.249 Matches (["normalize", "4x4", "linear", "system"], _)] => ()
1.250 - | _ => raise error "eqsystem.sml: refine relaxed triangular sys NoMatch";
1.251 + | _ => error "eqsystem.sml: refine relaxed triangular sys NoMatch";
1.252 (*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
1.253
1.254 val fmz = ["equalities [L * q_0 = c, \
1.255 @@ -760,7 +760,7 @@
1.256 *)
1.257 case matches of
1.258 [Matches (["triangular", "4x4", "linear", "system"], _)] => ()
1.259 - | _ => raise error "eqsystem.sml: refine relaxed triangular sys Matches";
1.260 + | _ => error "eqsystem.sml: refine relaxed triangular sys Matches";
1.261 val matches = refine fmz ["linear","system"];
1.262
1.263
1.264 @@ -874,7 +874,7 @@
1.265 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.266 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.267 case nxt of ("Specify_Method",_) => ()
1.268 - | _ => raise error "eqsystem.sml [EqSystem,normalize,2x2] specify";
1.269 + | _ => error "eqsystem.sml [EqSystem,normalize,2x2] specify";
1.270
1.271 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.272 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.273 @@ -884,7 +884,7 @@
1.274 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.275 case nxt of
1.276 (_, Subproblem ("Biegelinie", ["triangular", "2x2", "linear",_])) => ()
1.277 - | _ => raise error "eqsystem.sml me [EqSystem,normalize,2x2] SubProblem";
1.278 + | _ => error "eqsystem.sml me [EqSystem,normalize,2x2] SubProblem";
1.279
1.280 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.281 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.282 @@ -892,7 +892,7 @@
1.283 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.284 case nxt of
1.285 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
1.286 - | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
1.287 + | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
1.288
1.289 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.290 val PblObj {probl,...} = get_obj I pt [5];
1.291 @@ -912,14 +912,14 @@
1.292 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.293 case nxt of
1.294 (_, Check_Postcond ["triangular", "2x2", "linear", "system"]) => ()
1.295 - | _ => raise error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
1.296 + | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
1.297 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.298 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.299 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
1.300 -else raise error "eqsystem.sml me [EqSys...2x2] finished f2str f";
1.301 +else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
1.302 case nxt of
1.303 (_, End_Proof') => ()
1.304 - | _ => raise error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
1.305 + | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
1.306
1.307
1.308 "----------- me [linear,system] ..normalize..top_down_sub..-------";
1.309 @@ -941,7 +941,7 @@
1.310 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.311 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.312 case nxt of (_,Specify_Method ["EqSystem", "normalize", "2x2"]) => ()
1.313 - | _ => raise error "eqsystem.sml [linear,system] specify b";
1.314 + | _ => error "eqsystem.sml [linear,system] specify b";
1.315 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.316 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.317 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.318 @@ -950,10 +950,10 @@
1.319 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.320 if f2str f =
1.321 "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
1.322 -then () else raise error "eqsystem.sml me simpl. before SubProblem b";
1.323 +then () else error "eqsystem.sml me simpl. before SubProblem b";
1.324 case nxt of
1.325 (_, Subproblem ("Biegelinie", ["triangular", "2x2", "linear",_])) => ()
1.326 - | _ => raise error "eqsystem.sml me [linear,system] SubProblem b";
1.327 + | _ => error "eqsystem.sml me [linear,system] SubProblem b";
1.328
1.329 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.330 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.331 @@ -961,7 +961,7 @@
1.332 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.333 case nxt of
1.334 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
1.335 - | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
1.336 + | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
1.337
1.338 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.339 val PblObj {probl,...} = get_obj I pt [5];
1.340 @@ -981,15 +981,15 @@
1.341 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.342 case nxt of
1.343 (_, Check_Postcond ["triangular", "2x2", "linear", "system"]) => ()
1.344 - | _ => raise error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
1.345 + | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
1.346 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.347 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.348 if f2str f =
1.349 "[c = -1 * q_0 * L ^^^ 4 / (24 * EI * L), c_2 = 0]"
1.350 -then () else raise error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
1.351 +then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
1.352 case nxt of
1.353 (_, End_Proof') => ()
1.354 - | _ => raise error "eqsystem.sml me [EqSys...2x2] finished End_Proof'" b;
1.355 + | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'" b;
1.356
1.357
1.358 "----------- all systems from Biegelinie -------------------------";
1.359 @@ -1114,7 +1114,7 @@
1.360 term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_4 = 0, c_3 = 0]";
1.361 val SOME (t,_) = rewrite_set_ thy false order_system t;
1.362 if term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]" then ()
1.363 -else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed";
1.364 +else error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed";
1.365
1.366
1.367 "----- 7.70 with met normalize: ";
1.368 @@ -1133,7 +1133,7 @@
1.369 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.370 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.371 case nxt of (_,Apply_Method ["EqSystem", "normalize", "4x4"]) => ()
1.372 - | _ => raise error "eqsystem.sml [EqSystem,normalize,4x4] specify";
1.373 + | _ => error "eqsystem.sml [EqSystem,normalize,4x4] specify";
1.374 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.375 "bbbbbbbbbbbbbbbbbbbbbbbbbbbbb outcommented vvvvvvvvvvvvvvvvvvvvvv";
1.376 (*vvvWN080102 Exception- Match raised
1.377 @@ -1148,7 +1148,7 @@
1.378 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.379 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.380 if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]"
1.381 -then () else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by met changed";
1.382 +then () else error "eqsystem.sml: exp 7.70 normalize 4x4 by met changed";
1.383 --------------------------------------------------------------------------*)
1.384
1.385 "----- 7.70 with met top_down_: ";
1.386 @@ -1311,7 +1311,7 @@
1.387 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.388 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.389 case nxt of (_,Apply_Method ["EqSystem", "top_down_substitution", "4x4"]) => ()
1.390 - | _ => raise error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
1.391 + | _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
1.392 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.393 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.394 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.395 @@ -1320,7 +1320,7 @@
1.396 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.397 if nxt = ("End_Proof'", End_Proof') andalso
1.398 f2str f = "[c = L * q_0, c_2 = -1 * L ^^^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
1.399 -then () else raise error "eqsystem.sml: 7.70 with met top_down_: me";
1.400 +then () else error "eqsystem.sml: 7.70 with met top_down_: me";
1.401
1.402
1.403 "------- Bsp 7.71";