test/Tools/isac/OLDTESTS/subp-rooteq.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37981 b2877b9d455a
child 38058 ad0485155c0e
     1.1 --- a/test/Tools/isac/OLDTESTS/subp-rooteq.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/subp-rooteq.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -134,7 +134,7 @@
     1.4  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
     1.5  val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f;
     1.6  if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
     1.7 -else raise error "subp-rooteq.sml: new.behav. in  miniscript with mini-subpbl";
     1.8 +else error "subp-rooteq.sml: new.behav. in  miniscript with mini-subpbl";
     1.9  
    1.10  
    1.11  "---------------- solve_linear as rootpbl -----------------";
    1.12 @@ -177,7 +177,7 @@
    1.13    val nxt = ("End_Proof'",End_Proof') : string * tac*)
    1.14  val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f;
    1.15  if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
    1.16 -else raise error "subp-rooteq.sml: new.behav. in  solve_linear as rootpbl";
    1.17 +else error "subp-rooteq.sml: new.behav. in  solve_linear as rootpbl";
    1.18  
    1.19  
    1.20  "---------------- solve_plain_square as rootpbl -----------";
    1.21 @@ -210,7 +210,7 @@
    1.22  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.23  val  Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
    1.24  if snd nxt=End_Proof' andalso res="[x = -3, x = 3]" then ()
    1.25 -else raise error "subp-rooteq.sml: new.behav. in  solve_plain_square as rootpbl";
    1.26 +else error "subp-rooteq.sml: new.behav. in  solve_plain_square as rootpbl";
    1.27  
    1.28  
    1.29  
    1.30 @@ -283,7 +283,7 @@
    1.31  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.32  val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
    1.33  if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
    1.34 -else raise error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_linear";
    1.35 +else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_linear";
    1.36  
    1.37  
    1.38  
    1.39 @@ -357,7 +357,7 @@
    1.40  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.41  val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
    1.42  if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
    1.43 -else raise error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_plain_square";
    1.44 +else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_plain_square";
    1.45  
    1.46  
    1.47  writeln (pr_ptree pr_short pt);
    1.48 @@ -420,12 +420,12 @@
    1.49  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.50  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.51  if p = ([13],Res) then ()
    1.52 -else raise error ("subp-rooteq.sml: new.behav. in  \
    1.53 +else error ("subp-rooteq.sml: new.behav. in  \
    1.54  		 \root-eq + subpbl: solve_linear, p ="^(pos'2str p));
    1.55  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.56  val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
    1.57  if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
    1.58 -else raise error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_plain_square";
    1.59 +else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: solve_plain_square";
    1.60  
    1.61  
    1.62  
    1.63 @@ -485,7 +485,7 @@
    1.64  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.65  val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
    1.66  if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
    1.67 -else raise error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: no_met: square";
    1.68 +else error "subp-rooteq.sml: new.behav. in  root-eq + subpbl: no_met: square";
    1.69  
    1.70  
    1.71  
    1.72 @@ -533,7 +533,7 @@
    1.73  val (p,_,Form' (FormKF (_,_,_,_,f)),nxt,_,_) = 
    1.74      me nxt p c pt;
    1.75  if f="[x = 5]" andalso nxt=("End_Proof'",End_Proof') then ()
    1.76 -else raise error "subp-rooteq.sml: new.behav. in no_met in rootpbl -> linear ---";
    1.77 +else error "subp-rooteq.sml: new.behav. in no_met in rootpbl -> linear ---";
    1.78  
    1.79  
    1.80  refine fmz ["univariate","equation","test"];