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) =