1.1 --- a/src/smltest/IsacKnowledge/rational.sml	Thu Aug 31 10:33:44 2006 +0200
     1.2 +++ b/src/smltest/IsacKnowledge/rational.sml	Thu Aug 31 10:49:48 2006 +0200
     1.3 @@ -1990,7 +1990,7 @@
     1.4  
     1.5  val p = ([1,2,1,9],Res);
     1.6  getTactic 1 p;
     1.7 -val (_, tac, _) = pt_extract (pt, p)
     1.8 +val (_, tac, _) = pt_extract (pt, p);
     1.9  if tac = 
    1.10     Some (Rewrite("sym_real_plus_binom_times1",
    1.11  		 "?a ^^^ 2 + -1 * ?b ^^^ 2 = (?a + 1 * ?b) * (?a + -1 * ?b)"))
    1.12 @@ -2068,7 +2068,7 @@
    1.13  term2str t' = "1 * a * (1 * a) / (1 * (1 * a))" (*true*); 
    1.14  (*... can be canceled with
    1.15  real_mult_div_cancel2 ?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n"*)
    1.16 -(*
    1.17 +(* sml/ME/rewtools.sml:
    1.18  val rtas = reverse_deriv thy Atools_erls rules ro None t';
    1.19 -writeln(rtas2str rtas);
    1.20 +writeln(deri2str rtas);
    1.21  *)