1.1 --- a/test/Tools/isac/Knowledge/atools.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/atools.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -26,12 +26,12 @@
1.4 fun str2term str = (term_of o the o (parse thy )) str;
1.5 fun term2s t = Syntax.string_of_term (thy2ctxt thy) t;
1.6 val t = str2term "x";
1.7 -if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f";
1.8 +if occurs_in t t then "OK" else error "atools.sml: occurs_in x x -> f";
1.9
1.10 val t = str2term "x occurs_in x";
1.11 val SOME (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0;
1.12 if (term2s t') = "x occurs_in x = True" then ()
1.13 -else raise error "atools.sml: x occurs_in x = True ???";
1.14 +else error "atools.sml: x occurs_in x = True ???";
1.15
1.16 "------- some_occur_in";
1.17 some_occur_in [str2term"c",str2term"c_2"] (str2term"a + b + c");
1.18 @@ -40,14 +40,14 @@
1.19 val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;
1.20 if term2str t' =
1.21 "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 =\nTrue" then ()
1.22 -else raise error "atools.sml: some_occur_in true";
1.23 +else error "atools.sml: some_occur_in true";
1.24
1.25 val t = str2term "some_of [c_3, c_4] occur_in \
1.26 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
1.27 val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;
1.28 if term2str t' =
1.29 "some_of [c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
1.30 -else raise error "atools.sml: some_occur_in false";
1.31 +else error "atools.sml: some_occur_in false";
1.32
1.33
1.34 "----------- argument_of -----------------------------------------";
1.35 @@ -56,7 +56,7 @@
1.36 val t = str2term "argument_in (M_b x)";
1.37 val SOME (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0;
1.38 if term2s t' = "(argument_in M_b x) = x" then ()
1.39 -else raise error "atools.sml:(argument_in M_b x) = x ???";
1.40 +else error "atools.sml:(argument_in M_b x) = x ???";
1.41
1.42 "----------- sameFunId -------------------------------------------";
1.43 "----------- sameFunId -------------------------------------------";
1.44 @@ -91,7 +91,7 @@
1.45 \[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
1.46 val SOME (str, es) = eval_filter_sameFunId "" "Atools.filter'_sameFunId" p "";
1.47 if term2str es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n y x = c + L * x]) =\n[y' x = c + L * x]" then ()
1.48 -else raise error "atools.slm diff.behav. in filter_sameFunId";
1.49 +else error "atools.slm diff.behav. in filter_sameFunId";
1.50
1.51
1.52 "----------- boollist2sum ----------------------------------------";
1.53 @@ -114,7 +114,7 @@
1.54
1.55 val SOME (str, pred) = eval_boollist2sum "" "Atools.boollist2sum" t "";
1.56 if term2str pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then ()
1.57 -else raise error "atools.sml diff.behav. in eval_boollist2sum";
1.58 +else error "atools.sml diff.behav. in eval_boollist2sum";
1.59
1.60 trace_rewrite:=true;
1.61 val srls_ = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
1.62 @@ -122,7 +122,7 @@
1.63 val t = str2term
1.64 "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
1.65 case rewrite_set_ thy false srls_ t of SOME _ => ()
1.66 -| _ => raise error "atools.sml diff.rewrite boollist2sum";
1.67 +| _ => error "atools.sml diff.rewrite boollist2sum";
1.68 trace_rewrite:=false;
1.69
1.70