wneuper/isa: comparison test/Tools/isac/Knowledge/eqsystem.sml

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 "----------- occur_exactly_in ------------------------------------";
 val all = [str2term"c", str2term"c_2", str2term"c_3"];
 val t = str2term"0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
 if occur_exactly_in [str2term"c", str2term"c_2"] all t
-then () else raise error "eqsystem.sml occur_exactly_in 1";
+then () else error "eqsystem.sml occur_exactly_in 1";
 if not (occur_exactly_in [str2term"c", str2term"c_2", str2term"c_3"] all t)
-then () else raise error "eqsystem.sml occur_exactly_in 2";
+then () else error "eqsystem.sml occur_exactly_in 2";
 if not (occur_exactly_in [str2term"c_2"] all t)
-then () else raise error "eqsystem.sml occur_exactly_in 3";
+then () else error "eqsystem.sml occur_exactly_in 3";
 val t = str2term"[c,c_2] from_ [c,c_2,c_3] occur_exactly_in \
 		\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
 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 ()
-else raise error "eval_occur_exactly_in [c, c_2]";
+else error "eval_occur_exactly_in [c, c_2]";
 val t = str2term"[c,c_2,c_3] from_ [c,c_2,c_3] occur_exactly_in \
 		\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
 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 ()
-else raise error "eval_occur_exactly_in [c, c_2, c_3]";
+else error "eval_occur_exactly_in [c, c_2, c_3]";
 val t = str2term"[c_2] from_ [c,c_2,c_3] occur_exactly_in \
 		\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
 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 ()
-else raise error "eval_occur_exactly_in [c, c_2, c_3]";
+else error "eval_occur_exactly_in [c, c_2, c_3]";
 val t = str2term"[] from_ [c,c_2,c_3] occur_exactly_in 0";
 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
 if str = "[] from_ [c, c_2, c_3] occur_exactly_in 0 = True" then ()
-else raise error "eval_occur_exactly_in [c, c_2, c_3]";
+else error "eval_occur_exactly_in [c, c_2, c_3]";
 val t =
 str2term
 	"[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) /2";
 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
 if str = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in \
 	 \-1 * (q_0 * L ^^^ 2) / 2 = True" then ()
-else raise error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
+else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
 "----------- problems --------------------------------------------";
 "----------- problems --------------------------------------------";
 "----------- problems --------------------------------------------";
 			  Calc ("Groups.plus_class.plus", eval_binop "#add_"),
 			  Calc ("op =",eval_equal "#equal_")
 			  ];
 val SOME (t',_) = rewrite_set_ thy false testrls t;
 if term2str t' = "True" then ()
-else raise error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
+else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
 val SOME t = parse EqSystem.thy "solution L";
 atomty (term_of t);
 val SOME t = parse Biegelinie.thy "solution L";
 atomty (term_of t);
 			      Calc ("EqSystem.occur'_exactly'_in",
 				    eval_occur_exactly_in
 					"#eval_occur_exactly_in_")
 			      ]) t;
 if t = HOLogic.true_const then ()
-else raise error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
+else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
 "----------- rewrite-order ord_simplify_System -------------------";
 "----------- rewrite-order ord_simplify_System -------------------";
 "----------- rewrite-order ord_simplify_System -------------------";
 "M_b x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
 "--- add_commute ---";
 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",
 				       str2term"c * x") then ()
-else raise error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c * x) not#1";
+else error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c * x) not#1";
 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",
 				       str2term"c_2") then ()
-else raise error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c_2) not#2";
+else error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c_2) not#2";
 if ord_simplify_System false thy [] (str2term"c * x",
 				       str2term"c_2") then ()
-else raise error "integrate.sml, (c * x) < (c_2) not#3";
+else error "integrate.sml, (c * x) < (c_2) not#3";
 "--- mult_commute ---";
 if ord_simplify_System false thy [] (str2term"x * c",
 				       str2term"c * x") then ()
-else raise error "integrate.sml, (x * c) < (c * x) not#4";
+else error "integrate.sml, (x * c) < (c * x) not#4";
 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c",
 				       str2term"-1 * q_0 * c * (x ^^^ 2 / 2)")
-then () else raise error "integrate.sml, (. * .) < (. * .) not#5";
+then () else error "integrate.sml, (. * .) < (. * .) not#5";
 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c",
 				       str2term"c * -1 * q_0 * (x ^^^ 2 / 2)")
-then () else raise error "integrate.sml, (. * .) < (. * .) not#6";
+then () else error "integrate.sml, (. * .) < (. * .) not#6";
 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";
 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";
 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";
 	        \0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2]";
 val bdvs = [(str2term"bdv_1",str2term"c"),
 	    (str2term"bdv_2",str2term"c_2")];
 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
 if term2str t = "[0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2), 0 = c_2]"
-then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
+then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
 if term2str t = "[L * c + c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2), c_2 = 0]"
-then () else raise error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
+then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
 if term2str t = "[L * c + c_2 = q_0 * L ^^^ 2 / 2, c_2 = 0]"
-then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
+then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
 val SOME (t,_) = rewrite_set_ thy true order_system t;
 if term2str t = "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"
-then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
+then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
 	    \                                     -1 * q_0 / 24 * 0 ^^^ 4),\
 	    \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 +         \
 	    \                                     -1 * q_0 / 24 * L ^^^ 4)]";
 val SOME (t,_) = rewrite_set_ thy true norm_Rational t;
 if term2str t="[0 = c_2, 0 = c_2 + L * c + L ^^^ 4 * q_0 / (EI * 24)]"
-then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
+then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
 if term2str t = "[0 = c_2, 0 = q_0 * L ^^^ 4 / (24 * EI) + (L * c + c_2)]"
-then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
+then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
 if term2str t = "[c_2 = 0, L * c + c_2 = 0 + -1 * (q_0 * L ^^^ 4 / (24 * EI))]"
-then () else raise error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
+then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
 if term2str t = "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
-then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
+then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
 val xxx = rewrite_set_ thy true order_system t;
 if is_none xxx
-then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
+then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
 val e2__ = str2term "L * c + c_2 = q_0 * L ^^^ 2 / 2";
 val bdvs = [(str2term"bdv_1",str2term"c"),
 	    (str2term"bdv_2",str2term"c_2")];
 val SOME (e2__,_) = rewrite_terms_ thy dummy_ord Erls [e1__] e2__;
 if term2str e2__ = "L * c + 77 = q_0 * L ^^^ 2 / 2" then ()
-else raise error "eqsystem.sml top_down_substitution,2x2] subst";
+else error "eqsystem.sml top_down_substitution,2x2] subst";
 val SOME (e2__,_) =
 rewrite_set_inst_ thy true bdvs simplify_System_parenthesized e2__;
 if term2str e2__ = "77 + L * c = q_0 * L ^^^ 2 / 2" then ()
-else raise error "eqsystem.sml top_down_substitution,2x2] simpl_par";
+else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
 val SOME (e2__,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs e2__;
 if term2str e2__ = "c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L" then ()
-else raise error "eqsystem.sml top_down_substitution,2x2] isolate";
+else error "eqsystem.sml top_down_substitution,2x2] isolate";
 val t = str2term "[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]";
 val SOME (t,_) = rewrite_set_ thy true order_system t;
 if term2str t = "[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]" then ()
-else raise error "eqsystem.sml top_down_substitution,2x2] order_system";
+else error "eqsystem.sml top_down_substitution,2x2] order_system";
 if not (ord_simplify_System
 	    false thy []
 	    (str2term"[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]",
 	     str2term"[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]"))
-then () else raise error "eqsystem.sml, order_result rew_ord";
+then () else error "eqsystem.sml, order_result rew_ord";
 trace_rewrite:=true;
 trace_rewrite:=false;
 	    (str2term"bdv_4",str2term"c_4")];
 val SOME (t,_) =
 rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
 if term2str t = "[0 = c_4, 0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c_3 + c_4),\n\
 	        \ c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
-then () else raise error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
+then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
 if term2str t = "[c_4 = 0, \
 	        \L * c_3 + c_4 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2),\n \
 		\c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
-then () else raise error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
+then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
 if term2str t = "[c_4 = 0,\
 		\ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\
 		\ c + (c_2 + (c_3 + c_4)) = 0,\n\
 		\ c_2 + (c_3 + c_4) = 0]"
-then () else raise error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
+then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
 val SOME (t,_) = rewrite_set_ thy true order_system t;
 if term2str t = "[c_4 = 0,\
 		\ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\
 		\ c_2 + (c_3 + c_4) = 0,\n\
 		\ c + (c_2 + (c_3 + c_4)) = 0]"
-then () else raise error "eqsystem.sml rewrite in 4x4 order_system";
+then () else error "eqsystem.sml rewrite in 4x4 order_system";
 "----------- script [EqSystem,normalize,2x2] ---------------------";
 "----------- script [EqSystem,normalize,2x2] ---------------------";
 "----------- script [EqSystem,normalize,2x2] ---------------------";
 			   [Correct
 				"equalities\n [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\n  0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
 				Correct "solveForVars [c, c_2]"],
 			   Where = [],
 			   Relate = []})] => ()
-	      | _ => raise error "eqsystem.sml refine ['normalize','2x2'...]";
+	      | _ => error "eqsystem.sml refine ['normalize','2x2'...]";
 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
 	   "solveForVars [c, c_2]", "solution L"];
 val matches = refine fmz ["linear","system"];
 		       [Correct
 			    "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1\n       [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
 			    Correct
 				"[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]"],
 		       Relate = []})] => ()
-	      | _ => raise error "eqsystem.sml refine ['triangular','2x2'...]";
+	      | _ => error "eqsystem.sml refine ['triangular','2x2'...]";
 (*WN051014----------------------------------------------------------------
 the above 'val matches = refine fmz ["linear","system"]'
 didn't work anymore; we investigated in these steps:*)
 NoMatch (["2x2", "linear", "system"], _),
 NoMatch (["3x3", "linear", "system"], _),
 Matches (["4x4", "linear", "system"], _),
 NoMatch (["triangular", "4x4", "linear", "system"], _),
 Matches (["normalize", "4x4", "linear", "system"], _)] => ()
-| _ => raise error "eqsystem.sml: refine relaxed triangular sys NoMatch";
+| _ => error "eqsystem.sml: refine relaxed triangular sys NoMatch";
 (*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
 val fmz = ["equalities [L * q_0 = c,                                       \
 	   \            0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
 	   \            0 = c_3,                           \
 val matches = refine fmz ["triangular", "4x4", "linear","system"];
 (* print_depth 11; matches; print_depth 3;
 *)
 case matches of
 [Matches (["triangular", "4x4", "linear", "system"], _)] => ()
-| _ => raise error "eqsystem.sml: refine relaxed triangular sys Matches";
+| _ => error "eqsystem.sml: refine relaxed triangular sys Matches";
 val matches = refine fmz ["linear","system"];
 "----------- refine [2x2,linear,system] search error--------------";
 "----------- refine [2x2,linear,system] search error--------------";
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 case nxt of ("Specify_Method",_) => ()
-	  | _ => raise error "eqsystem.sml [EqSystem,normalize,2x2] specify";
+	  | _ => error "eqsystem.sml [EqSystem,normalize,2x2] specify";
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*);
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 case nxt of
 (_, Subproblem ("Biegelinie", ["triangular", "2x2", "linear",_])) => ()
-| _ => raise error "eqsystem.sml me [EqSystem,normalize,2x2] SubProblem";
+| _ => error "eqsystem.sml me [EqSystem,normalize,2x2] SubProblem";
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 case nxt of
 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
-| _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
+| _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val PblObj {probl,...} = get_obj I pt [5];
 (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
 (*[
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 case nxt of
 (_, Check_Postcond ["triangular", "2x2", "linear", "system"]) => ()
-| _ => raise error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
+| _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
-else raise error "eqsystem.sml me [EqSys...2x2] finished f2str f";
+else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
 case nxt of
 (_, End_Proof') => ()
-| _ => raise error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
+| _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
 "----------- me [linear,system] ..normalize..top_down_sub..-------";
 "----------- me [linear,system] ..normalize..top_down_sub..-------";
 "----------- me [linear,system] ..normalize..top_down_sub..-------";
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 case nxt of (_,Specify_Method ["EqSystem", "normalize", "2x2"]) => ()
-	  | _ => raise error "eqsystem.sml [linear,system] specify b";
+	  | _ => error "eqsystem.sml [linear,system] specify b";
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 if f2str f =
 "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
-then () else raise error "eqsystem.sml me simpl. before SubProblem b";
+then () else error "eqsystem.sml me simpl. before SubProblem b";
 case nxt of
 (_, Subproblem ("Biegelinie", ["triangular", "2x2", "linear",_])) => ()
-| _ => raise error "eqsystem.sml me [linear,system] SubProblem b";
+| _ => error "eqsystem.sml me [linear,system] SubProblem b";
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 case nxt of
 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
-| _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
+| _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val PblObj {probl,...} = get_obj I pt [5];
 (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
 (*[
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 case nxt of
 (_, Check_Postcond ["triangular", "2x2", "linear", "system"]) => ()
-| _ => raise error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
+| _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 if f2str f =
 "[c = -1 * q_0 * L ^^^ 4 / (24 * EI * L), c_2 = 0]"
-then () else raise error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
+then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
 case nxt of
 (_, End_Proof') => ()
-| _ => raise error "eqsystem.sml me [EqSys...2x2] finished End_Proof'" b;
+| _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'" b;
 "----------- all systems from Biegelinie -------------------------";
 "----------- all systems from Biegelinie -------------------------";
 "----------- all systems from Biegelinie -------------------------";
 rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
 term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_4 = 0, c_3 = 0]";
 val SOME (t,_) = rewrite_set_ thy false order_system t;
 if term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]" then ()
-else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed";
+else error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed";
 "----- 7.70 with met normalize: ";
 val fmz = ["equalities                                         \
 	    \[L * q_0 = c,                       \
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 case nxt of (_,Apply_Method ["EqSystem", "normalize", "4x4"]) => ()
-	  | _ => raise error "eqsystem.sml [EqSystem,normalize,4x4] specify";
+	  | _ => error "eqsystem.sml [EqSystem,normalize,4x4] specify";
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 "bbbbbbbbbbbbbbbbbbbbbbbbbbbbb outcommented vvvvvvvvvvvvvvvvvvvvvv";
 (*vvvWN080102 Exception- Match raised
 since assod Rewrite .. Rewrite'_Set
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]"
-then () else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by met changed";
+then () else error "eqsystem.sml: exp 7.70 normalize 4x4 by met changed";
 --------------------------------------------------------------------------*)
 "----- 7.70 with met top_down_: ";
 "--- scr [EqSystem,top_down_substitution,4x4] -- a saved trial";
 (*---vvv-this script failed with if ?!?-------------------------------------*)
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 case nxt of (_,Apply_Method ["EqSystem", "top_down_substitution", "4x4"]) => ()
-	  | _ => raise error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
+	  | _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 if nxt = ("End_Proof'", End_Proof') andalso
 f2str f = "[c = L * q_0, c_2 = -1 * L ^^^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
-then () else raise error "eqsystem.sml: 7.70 with met top_down_: me";
+then () else error "eqsystem.sml: 7.70 with met top_down_: me";
 "------- Bsp 7.71";
 states:=[];
 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",

branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38014	3e11e3c2dc42
child 38050	4c52ad406c20