*** empty log message ***
authorwneuper
Sun, 12 Oct 2003 16:24:54 +0200
changeset 970b1b5c1ee1f64
parent 969 734b78b26e1f
child 971 ab1d83d6f453
*** empty log message ***
src/sml/systest/script.sml
     1.1 --- a/src/sml/systest/script.sml	Sun Oct 12 16:24:54 2003 +0200
     1.2 +++ b/src/sml/systest/script.sml	Sun Oct 12 16:24:54 2003 +0200
     1.3 @@ -1,7 +1,9 @@
     1.4 -(* use"test-script.sml";
     1.5 +(* use"systest/script.sml";
     1.6 +   use"script.sml";
     1.7     WN.13.3.00
     1.8    *)
     1.9  
    1.10 +
    1.11  "         scripts: Variante 'funktional'               ";
    1.12  "############## Make_fun_by_new_variable ##############";
    1.13  "############## Make_fun_by_explicit ##############";
    1.14 @@ -26,9 +28,9 @@
    1.15  
    1.16  
    1.17  
    1.18 -" #################################################### 6.5.03";
    1.19 -"         scripts: Variante 'funktional'               6.5.03";
    1.20 -" #################################################### 6.5.03 ";
    1.21 +" ################################################# 6.5.03";
    1.22 +"         scripts: Variante 'funktional'            6.5.03";
    1.23 +" ################################################# 6.5.03 ";
    1.24  
    1.25  val c = (the o (parse DiffApp.thy)) 
    1.26    "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
    1.27 @@ -46,9 +48,9 @@
    1.28     \       bool_list_ (dropWhile (ident e_) rs_)])::bool list))";
    1.29  
    1.30  
    1.31 -"###################################################### 6.5.03";
    1.32 -"############## Make_fun_by_new_variable ############## 6.5.03";
    1.33 -"###################################################### 6.5.03";
    1.34 +"################################################### 6.5.03";
    1.35 +"############## Make_fun_by_new_variable ########### 6.5.03";
    1.36 +"################################################### 6.5.03";
    1.37  
    1.38  val sc = (the o (parse DiffApp.thy)) (*start interpretieren*)
    1.39    "Script Make_fun_by_new_variable (f_::real) (v_::real)     \
    1.40 @@ -183,7 +185,7 @@
    1.41  (*val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
    1.42  val (p,_,f,nxt,_,pt) = me (mI,m) e_pos'[1] EmptyPtree;*)
    1.43  
    1.44 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'), [], [])];
    1.45 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.46  val nxt = ("Model_Problem",
    1.47  	   Model_Problem ["sqroot-test","univariate","equation","test"]);
    1.48  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.49 @@ -268,8 +270,9 @@
    1.50  val l0 = [];
    1.51  " --------------- 1. ---------------------------------------------";
    1.52  val (pt,_) = cappend_atomic pt[1]e_istate e_term(Rewrite("test",""))(str2term ct,[])Complete;
    1.53 +(*12.10.03:*** Unknown theorem(s) "rroot_square_inv"
    1.54  val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
    1.55 -
    1.56 +*)
    1.57  
    1.58  
    1.59  val scr as (Script sc) =