1.1 --- a/src/sml/Scripts/rewrite.sml	Sat Aug 20 15:15:41 2005 +0200
     1.2 +++ b/src/sml/Scripts/rewrite.sml	Sat Aug 20 15:15:41 2005 +0200
     1.3 @@ -1,7 +1,8 @@
     1.4 -(* use"../Scripts/rewrite.sml";
     1.5 -   use"Scripts/rewrite.sml";
     1.6 -   use"rewrite.sml";
     1.7 -   *)
     1.8 +(* isac's rewriter
     1.9 +   (c) Walther Neuper 1999
    1.10 +
    1.11 +use"~/proto2/isac/src/sml/Scripts/rewrite.sml";
    1.12 +*)
    1.13  
    1.14  
    1.15  exception NO_REWRITE;
    1.16 @@ -47,14 +48,6 @@
    1.17  			       "   stored: "^(terms2str simpl_p'))
    1.18  		  else(); (t',simpl_p'))                  (* + uncond.rew. *)
    1.19  	    else 
    1.20 -	 (*if put_asm
    1.21 -	   then (if ! trace_rewrite andalso i < ! depth 
    1.22 -		 then writeln((idt"#"(i+1))^" asms accepted: "^(terms2str p')^
    1.23 -			      "   stored: "^(terms2str simpl_p'))
    1.24 -		 else(); (t',simpl_p'))
    1.25 -	   else (if ! trace_rewrite andalso i < ! depth 
    1.26 -		 then writeln((idt"#"(i+1))^" asms false: "^(terms2str p')) 
    1.27 -		 else(); raise NO_REWRITE)*)
    1.28  		(if ! trace_rewrite andalso i < ! depth 
    1.29  		 then writeln((idt"#"(i+1))^" asms false: "^(terms2str p')) 
    1.30  		 else(); raise NO_REWRITE)

     2.1 --- a/src/smltest/IsacKnowledge/integrate.sml	Sat Aug 20 15:15:41 2005 +0200
     2.2 +++ b/src/smltest/IsacKnowledge/integrate.sml	Sat Aug 20 15:15:41 2005 +0200
     2.3 @@ -82,10 +82,15 @@
     2.4  if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
     2.5  else raise error "integrate.sml: eval_new_c ???";
     2.6  
     2.7 -val t = str2t "(x ^^^ 2 / 2) is_new_c_free";
     2.8 -val Some (_,t') = eval_is_new_c_free 0 0 t 0;
     2.9 -if term2s t' = "x ^^^ 2 / 2 is_new_c_free = True" then ()
    2.10 -else raise error "integrate.sml: eval_new_c ???";
    2.11 +val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
    2.12 +val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
    2.13 +if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
    2.14 +else raise error "integrate.sml: matches new_c = False";
    2.15 +
    2.16 +val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
    2.17 +val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
    2.18 +if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
    2.19 +then () else raise error "integrate.sml: matches new_c = True";
    2.20  
    2.21  val conditions_in_integration =
    2.22  Rls {id="conditions_in_integration", 
    2.23 @@ -93,17 +98,15 @@
    2.24  			       rew_ord = ("termlessI",termlessI), 
    2.25  			       erls = Erls, 
    2.26  			       srls = Erls, calc = [],
    2.27 -			       rules = [(*Calc ("Integrate.is'_new'_c'_free", 
    2.28 -					      eval_is_new_c_free ""),*)
    2.29 -					Calc ("Tools.matches",eval_matches ""),
    2.30 +			       rules = [Calc ("Tools.matches",eval_matches ""),
    2.31  					Thm ("not_true",num_str not_true),
    2.32 -					Thm ("not_false",not_false)
    2.33 +					Thm ("not_false",num_str not_false)
    2.34  					],
    2.35  			       scr = EmptyScr};
    2.36  fun rewrit thm str = 
    2.37      fst (the (rewrite_inst_ Integrate.thy tless_true 
    2.38  			    conditions_in_integration true subs thm str));
    2.39 -
    2.40 +trace_rewrite := true;
    2.41  val str = rewrit add_new_c (str2t "x ^^^ 2 / 2"); term2s str;
    2.42  val str = rewrit add_new_c str; term2s str;
    2.43