1.1 --- a/test/Tools/isac/Knowledge/rational.sml	Thu Mar 10 17:05:09 2011 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Mon Mar 14 16:50:44 2011 +0100
     1.3 @@ -485,7 +485,6 @@
     1.4  val e186a = the (rewrite_set thy' false "cancel" e186a');
     1.5    is_expanded (parse_rat "14 * x * y");
     1.6    is_expanded (parse_rat "x * y");
     1.7 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
     1.8  if e186a = ("14 / 1", "[\"y * x ~= 0\"]") then ()
     1.9  else error "rational.sml cancel Schalk e186a";
    1.10  
    1.11 @@ -495,7 +494,7 @@
    1.12  writeln("c)");
    1.13  val e186c'="(144 * a^^^2 * b * c) / (12 * a * b * c )";
    1.14  val e186c = (the (rewrite_set thy' false "cancel" e186c'))
    1.15 -    handle e => OldGoals.print_exn e;
    1.16 +    handle e => print_exn_G e;
    1.17  val t = (term_of o the o (parse thy)) e186c';
    1.18  if e186c = ("12 * a / 1", "[\"12 * (c * (b * a)) ~= 0\"]") then ()
    1.19  else error "rational.sml cancel Schalk e186c";
    1.20 @@ -612,7 +611,6 @@
    1.21  if t = "(-5 + 3 * x) / 1" andalso asm = "[\"5 + 3 * x ~= 0\"]" then ()
    1.22  else error "rational.sml: new behav. in cancel wn01";
    1.23  
    1.24 -
    1.25  "-------- common_nominator_p ----------------------------";
    1.26  "-------- common_nominator_p ----------------------------";
    1.27  "-------- common_nominator_p ----------------------------";
    1.28 @@ -1839,7 +1837,6 @@
    1.29    ("Rational",["rational","simplification"],
    1.30     ["simplification","of_rationals"]);
    1.31  val p = e_pos'; val c = []; 
    1.32 -(*========== inhibit exn =======================================================
    1.33  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.34  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.35  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.36 @@ -1886,6 +1883,7 @@
    1.37  moveActiveRoot 1;
    1.38  autoCalculate 1 CompleteCalc;
    1.39  val ((pt,p),_) = get_calc 1; show_pt pt;
    1.40 +(*========== inhibit exn 110314 ================================================
    1.41  (*with explicit script done already... and removed [1,..] at below...
    1.42  interSteps 1 ([1],Res);
    1.43  val ((pt,p),_) = get_calc 1; show_pt pt;
    1.44 @@ -1907,12 +1905,13 @@
    1.45  WN060905*)
    1.46  case tac of SOME (Rewrite ("sym_real_add_mult_distrib2", _)) => ()
    1.47  | _ => error "rational.sml: getTactic, sym_real_plus_binom_times1";
    1.48 +============ inhibit exn 110314 ==============================================*)
    1.49  
    1.50  
    1.51  "-------- investigate rulesets for cancel_p -------------";
    1.52  "-------- investigate rulesets for cancel_p -------------";
    1.53  "-------- investigate rulesets for cancel_p -------------";
    1.54 -val thy = Rational.thy;
    1.55 +val thy = @{theory "Rational"};
    1.56  "---------------- (a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)";
    1.57  val t = str2term "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)";
    1.58  val tt = str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"(*numerator only*);
    1.59 @@ -1962,7 +1961,7 @@
    1.60  "-------- investigate format of factout_ and factout_p_ -";
    1.61  "-------- investigate format of factout_ and factout_p_ -";
    1.62  val {rules, rew_ord = (_,ro),...} = rep_rls (assoc_rls "make_polynomial");
    1.63 -val (thy, eval_rls) = (Rational.thy, Atools_erls)(*see 'fun init_state'*);
    1.64 +val (thy, eval_rls) = (@{theory "Rational"}, Atools_erls)(*see 'fun init_state'*);
    1.65  val Rrls {scr = Rfuns {init_state,...},...} = assoc_rls "cancel_p";
    1.66  
    1.67  "----- see Rational.ML, local cancel_p, fun init_state";
    1.68 @@ -1986,7 +1985,6 @@
    1.69  *)
    1.70  
    1.71  
    1.72 -
    1.73  "-------- SK 060904 ----------------------------------------------";
    1.74  "----- order on polynomials -- input + output";
    1.75  val thy = @{theory "Isac"};
    1.76 @@ -2008,16 +2006,16 @@
    1.77  else error "rational.sml SK060904-1a worked since 0707xx";
    1.78  
    1.79  "----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
    1.80 -val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /" ^
    1.81 -"(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
    1.82 +val t = str2term ("(9 * a ^^^ 2 + -16 * b ^^^ 2) /" ^
    1.83 +"(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))");
    1.84  val SOME (t',_) = cancel_p_ thy t; 
    1.85  if term2str t' = "1 / (4 * c + 3 * e)" then ()
    1.86  else error "rational.sml SK060904-1b";
    1.87  
    1.88  
    1.89  "----- SK060904-2a non-termination of add_fraction_p_";
    1.90 -val t = str2term " (a + b * x) / (a + -1 * (b * x)) +  " ^
    1.91 -		 " (-1 * a + b * x) / (a + b * x)      ";
    1.92 +val t = str2term (" (a + b * x) / (a + -1 * (b * x)) +  " ^
    1.93 +		  " (-1 * a + b * x) / (a + b * x)      ");
    1.94  (* nonterm.SK
    1.95  val SOME (t',_) = rewrite_set_ thy false common_nominator_p t;
    1.96  
    1.97 @@ -2078,10 +2076,3 @@
    1.98  "    Try (Rewrite_Set discard_parentheses False))               " ^
    1.99  "   t_t)"
   1.100  );
   1.101 -
   1.102 -============ inhibit exn =====================================================*)
   1.103 -
   1.104 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
   1.105 -
   1.106 -
   1.107 -