test/Tools/isac/OLDTESTS/scriptnew.sml
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37984 972a73d7c50b
child 38043 6a36acec95d9
     1.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml	Tue Sep 28 08:58:06 2010 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml	Tue Sep 28 09:06:56 2010 +0200
     1.3 @@ -77,12 +77,12 @@
     1.4  val (p,_,f,nxt,_,pt) = me nxt p c pt;
     1.5  (*"#0"*)
     1.6  if p=([4],Res) then ()
     1.7 -else raise error ("new behaviour in 30.4.02 Testterm: p="^(pos'2str p));
     1.8 +else error ("new behaviour in 30.4.02 Testterm: p="^(pos'2str p));
     1.9  (*----script 666 ------------------------------------------------*)
    1.10  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.11  (*"#0"*)
    1.12  if nxt=("End_Proof'",End_Proof') then ()
    1.13 -else raise error "new behaviour in 30.4.02 Testterm: End_Proof";
    1.14 +else error "new behaviour in 30.4.02 Testterm: End_Proof";
    1.15  
    1.16  
    1.17  
    1.18 @@ -149,7 +149,7 @@
    1.19  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.20  if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"a = 0 ^^^ 2"))) andalso
    1.21     nxt=("End_Proof'",End_Proof') then ()
    1.22 -else raise error "different behaviour test 9.5.02 Testeq: While Try Repeat @@";
    1.23 +else error "different behaviour test 9.5.02 Testeq: While Try Repeat @@";
    1.24  
    1.25  
    1.26  
    1.27 @@ -198,7 +198,7 @@
    1.28  val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
    1.29  if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"[a = 0 ^^^ 2]"))) andalso
    1.30     nxt=("End_Proof'",End_Proof') then ()
    1.31 -else raise error "different behaviour in test 11.5.02 Testeq: let e_e =... in [e_]";
    1.32 +else error "different behaviour in test 11.5.02 Testeq: let e_e =... in [e_]";
    1.33  
    1.34  
    1.35  
    1.36 @@ -290,7 +290,7 @@
    1.37  (* nxt = ("Check_Postcond",Check_Postcond ("Test.thy","sqrt-equ-test"));*)
    1.38  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.39  if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))
    1.40 -then raise error "scriptnew.sml 1: me + tacs from script: new behaviour" 
    1.41 +then error "scriptnew.sml 1: me + tacs from script: new behaviour" 
    1.42  else ();
    1.43  "--- 15<> ---";
    1.44  (* val nxt = ("End_Proof'",End_Proof');*)
    1.45 @@ -375,7 +375,7 @@
    1.46  
    1.47  (*FIXXXXXXXXXXXXXXXXXXXXXXXME reestablish check:
    1.48  if f= Form'(FormKF(~1,EdUndef,1,Nundef,"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"))
    1.49 -then() else raise error "new behaviour in test-example 1.norm sqrt-equ-test";
    1.50 +then() else error "new behaviour in test-example 1.norm sqrt-equ-test";
    1.51  #################################################*)
    1.52  
    1.53  (* use"../tests/scriptnew.sml";
    1.54 @@ -411,7 +411,7 @@
    1.55  if asms = [(str2term "0 <= 9 + 4 * x",[1]),
    1.56  	   (str2term "0 <= x",[1]),
    1.57  	   (str2term "0 <= -3 + x",[1])] then ()
    1.58 -else raise error "scriptnew.sml diff.behav. in sqrt assumptions 1";
    1.59 +else error "scriptnew.sml diff.behav. in sqrt assumptions 1";
    1.60  
    1.61  val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.62  val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.63 @@ -425,7 +425,7 @@
    1.64  	   (str2term "0 <= -3 + x",[1]),
    1.65  	   (str2term "0 <= x ^^^ 2 + -3 * x",[6]),
    1.66  	   (str2term "0 <= 6 + x",[6])] then ()
    1.67 -else raise error "scriptnew.sml diff.behav. in sqrt assumptions 2";
    1.68 +else error "scriptnew.sml diff.behav. in sqrt assumptions 2";
    1.69  
    1.70  val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.71  val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.72 @@ -442,7 +442,7 @@
    1.73    ("Check_Postcond",Check_Postcond ["linear","univariate","equation","test"])*)
    1.74  val asms = get_assumptions_ pt p;
    1.75  if asms = [] then ()
    1.76 -else raise error "scriptnew.sml diff.behav. in sqrt assumptions 3";
    1.77 +else error "scriptnew.sml diff.behav. in sqrt assumptions 3";
    1.78  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.79  (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
    1.80  
    1.81 @@ -468,7 +468,7 @@
    1.82  val Form' (FormKF (_,_,_,_,ff)) = f;
    1.83  if ff="[x = -12 / 5]"
    1.84  then writeln("there should be L = []\nthere should be L = []\nthere should be L = []\nthere should be L = []\nthere should be L = []\n")
    1.85 -else raise error "diff.behav. in scriptnew.sml; root-eq: L = []";
    1.86 +else error "diff.behav. in scriptnew.sml; root-eq: L = []";
    1.87  
    1.88  val asms = get_assumptions_ pt p;
    1.89  if asms = [(str2term "0 <= 9 + 4 * (-12 / 5)",[]),
    1.90 @@ -476,7 +476,7 @@
    1.91  	   (str2term "0 <= -3 + -12 / 5", []),
    1.92  	   (str2term "0 <= (-12 / 5) ^^^ 2 + -3 * (-12 / 5)", []),
    1.93  	   (str2term "0 <= 6 + -12 / 5", [])] then ()
    1.94 -else raise error "scriptnew.sml diff.behav. in sqrt assumptions 4";
    1.95 +else error "scriptnew.sml diff.behav. in sqrt assumptions 4";
    1.96  
    1.97  
    1.98  "------------------ script with Map, Subst (biquadr.equ.)---------";