1.1 --- a/src/smltest/IsacKnowledge/integrate.sml	Sat Aug 20 19:10:30 2005 +0200
     1.2 +++ b/src/smltest/IsacKnowledge/integrate.sml	Sat Aug 20 21:20:16 2005 +0200
     1.3 @@ -15,9 +15,8 @@
     1.4  "----------- test new_c ------------------------------------------";
     1.5  "----------- integrate by ruleset --------------------------------";
     1.6  "----------- check probem type -----------------------------------";
     1.7 -"----------- check method [Diff,integration] ---------------------";
     1.8 -"----------- me method [Diff,integration] ---------------------";
     1.9 -"----------- check method [Diff,integration,named] ---------------";
    1.10 +"----------- check Scripts ---------------------------------------";
    1.11 +"----------- me method [Diff,integration] ------------------------";
    1.12  "-----------------------------------------------------------------";
    1.13  "-----------------------------------------------------------------";
    1.14  "-----------------------------------------------------------------";
    1.15 @@ -155,30 +154,26 @@
    1.16  case #cas pbl of Some (Const ("Integrate.Integrate",_) $ _) => ()
    1.17  	 | _ => raise error "integrate.sml: Integrate.Integrate ???";
    1.18  
    1.19 -"----------- check method [Diff,integration] ---------------------";
    1.20 -"----------- check method [Diff,integration] ---------------------";
    1.21 -"----------- check method [Diff,integration] ---------------------";
    1.22 -show_mets();
    1.23 -(*
    1.24 +
    1.25 +"----------- check Scripts ---------------------------------------";
    1.26 +"----------- check Scripts ---------------------------------------";
    1.27 +"----------- check Scripts ---------------------------------------";
    1.28  val str = 
    1.29  "Script IntegrationScript (f_::real) (v_::real) =               \
    1.30 -\  (let t_ = (Integral f_ D v_)::real                           \
    1.31 -\   in (Rewrite_Set_Inst [(bdv,v_)] integration False t_::real))";
    1.32 +\  (let t_ = Integral f_ D v_                                 \
    1.33 +\   in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))";
    1.34  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.35 +atomty thy sc;
    1.36  
    1.37  val str = 
    1.38 -"Script IntegrationScript (f_::real) (v_::real) =               \
    1.39 -\  (let t_ = (Integral f_ D v_)::real                           \
    1.40 -\   in t_)";
    1.41 +"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \
    1.42 +\  (let t_ = (F_ = Integral f_ D v_)                                 \
    1.43 +\   in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)";
    1.44  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.45 -val str = 
    1.46 -"Rewrite_Set_Inst [(bdv,v_)] integration False (t_::real)";
    1.47 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.48 +atomty thy sc;
    1.49 +show_mets();
    1.50  
    1.51  
    1.52 -atomty thy sc;
    1.53 -###############################################################*)
    1.54 -
    1.55  "----------- me method [Diff,integration] ---------------------";
    1.56  "----------- me method [Diff,integration] ---------------------";
    1.57  "----------- me method [Diff,integration] ---------------------";
    1.58 @@ -195,18 +190,8 @@
    1.59  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.60  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.61  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.62 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.63  val (p,_,f,nxt,_,pt) = me nxt p c pt;(*---> Empty_Tac*)
    1.64  
    1.65  
    1.66  
    1.67 -
    1.68 -
    1.69 -"----------- check method [Diff,integration,named] ---------------";
    1.70 -"----------- check method [Diff,integration,named] ---------------";
    1.71 -"----------- check method [Diff,integration,named] ---------------";
    1.72 -val str = 
    1.73 -"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \
    1.74 -\  (F_ = Integral f_ D v_)";
    1.75 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.76 -atomty thy sc;
    1.77 -