1.1 --- a/src/smltest/IsacKnowledge/rational.sml	Wed Aug 30 18:50:46 2006 +0200
     1.2 +++ b/src/smltest/IsacKnowledge/rational.sml	Thu Aug 31 08:27:39 2006 +0200
     1.3 @@ -2045,7 +2045,13 @@
     1.4  if length newnds = 12 then ()
     1.5  else raise error "rational.sml: interSteps cancel_p rev_rew_p";
     1.6  
     1.7 -getTactic 1 ([1,2,1,9],Res);
     1.8 +val p = ([1,2,1,9],Res);
     1.9 +getTactic 1 p;
    1.10 +val (_, tac, _) = pt_extract (pt, p)
    1.11 +if tac = 
    1.12 +   Some (Rewrite("sym_real_plus_binom_times1",
    1.13 +		 "?a ^^^ 2 + -1 * ?b ^^^ 2 = (?a + 1 * ?b) * (?a + -1 * ?b)"))
    1.14 +then () else raise error "rational.sml: getTactic, sym_real_plus_binom_times1";
    1.15  
    1.16  
    1.17  "-------- investigate rulesets for cancel_p ----------------------";