1.1 --- a/test/Tools/isac/Knowledge/diffapp.sml	Mon Sep 06 16:56:22 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml	Mon Sep 06 17:07:28 2010 +0200
     1.3 @@ -448,14 +448,14 @@
     1.4     \ (let e_e = (hd o (filterVar m_)) rs_;              \
     1.5     \      t_ = (if 1 < length_ rs_                            \
     1.6     \           then (SubProblem (Reals_,[make,function],[no_met])\
     1.7 -   \                     [real_ m_, real_ v_v, bool_list_ rs_])\
     1.8 +   \                     [REAL m_, REAL v_v, BOOL_LIST rs_])\
     1.9     \           else (hd rs_));                                \
    1.10     \      (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
    1.11     \                                [Isac,maximum_on_interval])\
    1.12 -   \                               [bool_ t_, real_ v_v, real_set_ itv_]\
    1.13 +   \                               [BOOL t_, REAL v_v, REAL_SET itv_]\
    1.14     \ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values])   \
    1.15 -   \      [real_ mx_, real_ (Rhs t_), real_ v_v, real_ m_,     \
    1.16 -   \       bool_list_ (dropWhile (ident e_e) rs_)])::bool list))";
    1.17 +   \      [REAL mx_, REAL (Rhs t_), REAL v_v, REAL m_,     \
    1.18 +   \       BOOL_LIST (dropWhile (ident e_e) rs_)])::bool list))";
    1.19  
    1.20  val fix_ = (str2term "fix_::bool list", 
    1.21  	    str2term "[r=Arbfix]");
    1.22 @@ -494,21 +494,21 @@
    1.23  val t = str2term 
    1.24  	    "(if 1 < length_ rs_                            \
    1.25     \           then (SubProblem (Reals_,[make,function],[no_met])\
    1.26 -   \                     [real_ m_, real_ v_v, bool_list_ rs_])\
    1.27 +   \                     [REAL m_, REAL v_v, BOOL_LIST rs_])\
    1.28     \           else (hd rs_))";
    1.29  val s = subst_atomic env t;
    1.30  term2str s;
    1.31  "if 1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]\
    1.32  \then SubProblem (Reals_, [make, function], [no_met])\
    1.33 -\      [real_ A, real_ b,\
    1.34 -\       bool_list_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]\
    1.35 +\      [REAL A, REAL b,\
    1.36 +\       BOOL_LIST [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]\
    1.37  \else hd [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
    1.38  val SOME (s',_) = rewrite_set_ thy false list_rls s;
    1.39  val s'' = term2str s';
    1.40  if s'' = 
    1.41  "SubProblem (Reals_, [make, function], [no_met])\n\
    1.42 -\ [real_ A, real_ b,\n\
    1.43 -\  bool_list_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]" then ()
    1.44 +\ [REAL A, REAL b,\n\
    1.45 +\  BOOL_LIST [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]" then ()
    1.46  else raise error "new behaviour with list_rls 1.3.";
    1.47  val env = env @ [(str2term "t_::bool",
    1.48  		  str2term "A = (2*sqrt(r^^^2-(b/2)^^^2)) * b")];
    1.49 @@ -526,7 +526,7 @@
    1.50     \      vs_ = dropWhile (ident f_) (Vars h_);                \
    1.51     \      v_1 = hd (dropWhile (ident v_v) vs_);                \
    1.52     \      (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\
    1.53 -   \                          [bool_ e_1, real_ v_1])\
    1.54 +   \                          [BOOL e_1, REAL v_1])\
    1.55     \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
    1.56  val f_ = (str2term "f_::real", 
    1.57  	  str2term "A");
    1.58 @@ -584,11 +584,11 @@
    1.59  
    1.60  (*--- 5.line in script ---*)
    1.61  val t = str2term "(SubProblem(Reals_,[univar,equation],[no_met])\
    1.62 -		 \           [bool_ e_1, real_ v_1])";
    1.63 +		 \           [BOOL e_1, REAL v_1])";
    1.64  val s = subst_atomic env t;
    1.65  term2str s;
    1.66  "SubProblem (Reals_, [univar, equation], [no_met])\n\
    1.67 -\ [bool_ ((a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2), real_ a]";
    1.68 +\ [BOOL ((a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2), REAL a]";
    1.69  val env = env @ [(str2term "s_1::bool list", 
    1.70  		  str2term "[a = 2 * sqrt (r^^^2 - (b/2)^^^2)]")];
    1.71  
    1.72 @@ -620,9 +620,9 @@
    1.73     \     e_1 = (hd o (filterVar v_1)) es_;            \
    1.74     \     e_2 = (hd o (filterVar v_2)) es_;            \
    1.75     \  (s_1::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
    1.76 -   \                    [bool_ e_1, real_ v_1]);\
    1.77 +   \                    [BOOL e_1, REAL v_1]);\
    1.78     \  (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
    1.79 -   \                    [bool_ e_2, real_ v_2])\
    1.80 +   \                    [BOOL e_2, REAL v_2])\
    1.81     \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";
    1.82  val f_ = (str2term "f_::real", 
    1.83  	  str2term "A");
    1.84 @@ -715,21 +715,21 @@
    1.85  
    1.86  (*--- 8.line in script ---*)
    1.87  val t = str2term "(SubProblem (Reals_,[univar,equation],[no_met])\
    1.88 -		 \            [bool_ e_1, real_ v_1])";
    1.89 +		 \            [BOOL e_1, REAL v_1])";
    1.90  val s = subst_atomic env t;
    1.91  term2str s;
    1.92  "SubProblem (Reals_, [univar, equation], [no_met])\
    1.93 -	    \ [bool_ (a / 2 = r * sin alpha), real_ a]";
    1.94 +	    \ [BOOL (a / 2 = r * sin alpha), REAL a]";
    1.95  val s_1 = str2term "[a = 2*r*sin alpha]";
    1.96  val env = env @ [(str2term "s_1::bool list", s_1)];
    1.97  
    1.98  (*--- 9.line in script ---*)
    1.99  val t = str2term "(SubProblem (Reals_,[univar,equation],[no_met])\
   1.100 -   \                    [bool_ e_2, real_ v_2])";
   1.101 +   \                    [BOOL e_2, REAL v_2])";
   1.102  val s = subst_atomic env t;
   1.103  term2str s;
   1.104  "SubProblem (Reals_, [univar, equation], [no_met])\
   1.105 -	    \ [bool_ (b / 2 = r * cos alpha), real_ b]";
   1.106 +	    \ [BOOL (b / 2 = r * cos alpha), REAL b]";
   1.107  val s_2 = str2term "[b = 2*r*cos alpha]";
   1.108  val env = env @ [(str2term "s_2::bool list", s_2)];
   1.109