test/Tools/isac/ProgLang/rewrite.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 38030 95d956108461
child 38036 02a9b2540eb7
     1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -203,21 +203,21 @@
     1.4  val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
     1.5  writeln "----------- rewrite_terms_  1---------------------------";
     1.6  if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
     1.7 -else raise error "rewrite.sml rewrite_terms_ [x = 0]";
     1.8 +else error "rewrite.sml rewrite_terms_ [x = 0]";
     1.9  
    1.10  val equs = [str2term "M_b 0 = 0"];
    1.11  val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
    1.12  val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
    1.13  writeln "----------- rewrite_terms_  2---------------------------";
    1.14  if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
    1.15 -else raise error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
    1.16 +else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
    1.17  
    1.18  val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
    1.19  val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
    1.20  val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
    1.21  writeln "----------- rewrite_terms_  3---------------------------";
    1.22  if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
    1.23 -else raise error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
    1.24 +else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
    1.25  
    1.26  
    1.27  "----------- rewrite_inst_ bdvs -------------------------";
    1.28 @@ -240,7 +240,7 @@
    1.29  		  false bdvs (num_str @{separate_bdvs_add) t;
    1.30  (writeln o term2str) t;
    1.31  if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
    1.32 -then () else raise error "rewrite.sml rewrite_inst_ bdvs";
    1.33 +then () else error "rewrite.sml rewrite_inst_ bdvs";
    1.34  trace_rewrite:=true;
    1.35  trace_rewrite:=false;--------------------------------------------*)
    1.36