val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 case nxt of (_,Apply_Method ["DiffApp","max_by_calculus"] ) => ()

 case nxt of (_,Apply_Method ["DiffApp","max_by_calculus"] ) => ()

 	  | _ => raise error "diffapp.sml: max-exp me, nxt = Apply_Method";

 	  | _ => raise error "diffapp.sml: max-exp me, nxt = Apply_Method";

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = ("Subproblem",Subproblem ("DiffApp.thy",["make","function"]))*)

 (*val nxt = ("Subproblem",Subproblem ("DiffApp.thy",["make","function"]))*)

 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn_G e;

 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn_G e;

 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["make","function"])*)

 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["make","function"])*)

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 val (p,_,f,nxt,_,pt) = me nxt p c pt;

 (*val nxt = ("Model_Problem",Model_Problem ["by_explicit","make","function"])*)

 (*val nxt = ("Model_Problem",Model_Problem ["by_explicit","make","function"])*)

 (*--- 1.line in script ---*)

 (*--- 1.line in script ---*)

 val t = str2term "(hd o (filterVar m_)) (rs_::bool list)";

 val t = str2term "(hd o (filterVar m_)) (rs_::bool list)";

 val s = subst_atomic env t;

 val s = subst_atomic env t;

 term2str s;

 term2str s;

 "(hd o filterVar A) [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";

 "(hd o filterVar A) [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";

 val s'' = term2str s';

 val s'' = term2str s';

 if s''="A = a * b" then () else raise error "new behaviour with list_rls 1.1.";

 if s''="A = a * b" then () else raise error "new behaviour with list_rls 1.1.";

 val env = env @ [(str2term "e_::bool",str2term "A = a * b")];

 val env = env @ [(str2term "e_::bool",str2term "A = a * b")];

 (*--- 2.line: condition alone ---*)

 (*--- 2.line: condition alone ---*)

 val t = str2term "1 < length_ (rs_::bool list)";

 val t = str2term "1 < length_ (rs_::bool list)";

 val s = subst_atomic env t;

 val s = subst_atomic env t;

 term2str s;

 term2str s;

 "1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";

 "1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";

 val s'' = term2str s';

 val s'' = term2str s';

 if s''="True" then () else raise error "new behaviour with list_rls 1.2.";

 if s''="True" then () else raise error "new behaviour with list_rls 1.2.";

 (*--- 2.line in script ---*)

 (*--- 2.line in script ---*)

 val t = str2term 

 val t = str2term 

 "if 1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]\

 "if 1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]\

 \then SubProblem (Reals_, [make, function], [no_met])\

 \then SubProblem (Reals_, [make, function], [no_met])\

 \      [real_ A, real_ b,\

 \      [real_ A, real_ b,\

 \       bool_list_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]\

 \       bool_list_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]\

 \else hd [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";

 \else hd [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";

 val s'' = term2str s';

 val s'' = term2str s';

 if s'' = 

 if s'' = 

 "SubProblem (Reals_, [make, function], [no_met])\n\

 "SubProblem (Reals_, [make, function], [no_met])\n\

 \ [real_ A, real_ b,\n\

 \ [real_ A, real_ b,\n\

 \  bool_list_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]" then ()

 \  bool_list_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]" then ()

 val t = str2term "(hd o (filterVar v_)) (eqs_::bool list)";

 val t = str2term "(hd o (filterVar v_)) (eqs_::bool list)";

 val s = subst_atomic env t;

 val s = subst_atomic env t;

 term2str s;

 term2str s;

 val t = str2term 

 val t = str2term 

      "(hd o filterVar b) [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";

      "(hd o filterVar b) [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";

 val s' = term2str t';

 val s' = term2str t';

 if s' = "A = a * b" then () else raise error "new behaviour with list_rls 2.1";

 if s' = "A = a * b" then () else raise error "new behaviour with list_rls 2.1";

 val env = env @ [(str2term "h_::bool", str2term s')];

 val env = env @ [(str2term "h_::bool", str2term s')];

 (*--- 2.line in script ---*)

 (*--- 2.line in script ---*)

 val t = str2term 

 val t = str2term 

 	    "hd (dropWhile (ident (A = a * b))\

 	    "hd (dropWhile (ident (A = a * b))\

 	    \     [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2])";

 	    \     [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2])";

 mem_rls "dropWhile_Cons" list_rls;

 mem_rls "dropWhile_Cons" list_rls;

 mem_rls "Atools.ident" list_rls;

 mem_rls "Atools.ident" list_rls;

 val s' = term2str t';

 val s' = term2str t';

 if s' = "(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2" then () 

 if s' = "(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2" then () 

 else raise error "new behaviour with list_rls 2.2";

 else raise error "new behaviour with list_rls 2.2";

 val env = env @ [(str2term "e_1::bool", str2term s')];

 val env = env @ [(str2term "e_1::bool", str2term s')];

 (*--- 3.line in script ---*)

 (*--- 3.line in script ---*)

 val t = str2term "dropWhile (ident f_) (Vars (h_::bool))";

 val t = str2term "dropWhile (ident f_) (Vars (h_::bool))";

 val s = subst_atomic env t;

 val s = subst_atomic env t;

 term2str s;

 term2str s;

 val t = str2term "dropWhile (ident A) (Vars (A = a * b))";

 val t = str2term "dropWhile (ident A) (Vars (A = a * b))";

 val s' = term2str t';

 val s' = term2str t';

 if s' = "[a, b]" then () else raise error "new behaviour with list_rls 2.3";

 if s' = "[a, b]" then () else raise error "new behaviour with list_rls 2.3";

 val env = env @ [(str2term "vs_::real list", str2term s')];

 val env = env @ [(str2term "vs_::real list", str2term s')];

 (*--- 4.line in script ---*)

 (*--- 4.line in script ---*)

 val t = str2term "hd (dropWhile (ident v_) vs_)";

 val t = str2term "hd (dropWhile (ident v_) vs_)";

 val s = subst_atomic env t;

 val s = subst_atomic env t;

 term2str s;

 term2str s;

 val t = str2term "hd (dropWhile (ident b) [a, b])";

 val t = str2term "hd (dropWhile (ident b) [a, b])";

 val s' = term2str t';

 val s' = term2str t';

 if s' = "a" then () else raise error "new behaviour with list_rls 2.4.";

 if s' = "a" then () else raise error "new behaviour with list_rls 2.4.";

 val env = env @ [(str2term "v_1::real", str2term s')];

 val env = env @ [(str2term "v_1::real", str2term s')];

 (*--- 5.line in script ---*)

 (*--- 5.line in script ---*)

 term2str s;

 term2str s;

 val t = str2term 

 val t = str2term 

 "Substitute [(a = (rhs o hd) [a = 2 * sqrt (r ^^^ 2 - (b / 2) ^^^ 2)])]\n\

 "Substitute [(a = (rhs o hd) [a = 2 * sqrt (r ^^^ 2 - (b / 2) ^^^ 2)])]\n\

 \ (A = a * b)";

 \ (A = a * b)";

 mem_rls "Tools.rhs" list_rls;

 mem_rls "Tools.rhs" list_rls;

 val s' = term2str t';

 val s' = term2str t';

 if s' = "Substitute [a = 2 * sqrt (r ^^^ 2 - (b / 2) ^^^ 2)] (A = a * b)" 

 if s' = "Substitute [a = 2 * sqrt (r ^^^ 2 - (b / 2) ^^^ 2)] (A = a * b)" 

 then () else raise error "new behaviour with list_rls 2.6.";

 then () else raise error "new behaviour with list_rls 2.6.";

 val s = subst_atomic env t;

 val s = subst_atomic env t;

 term2str s;

 term2str s;

 val t = str2term 

 val t = str2term 

 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";

 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";

 trace_rewrite:=true;

 trace_rewrite:=true;

 trace_rewrite:=false;

 trace_rewrite:=false;

 val s' = term2str t';

 val s' = term2str t';

 if s' = "A = a * b" then() else raise error "new behaviour with list_rls 3.1.";

 if s' = "A = a * b" then() else raise error "new behaviour with list_rls 3.1.";

 val env = env @ [(str2term "h_::bool", str2term s')];

 val env = env @ [(str2term "h_::bool", str2term s')];

 val s = subst_atomic env t;

 val s = subst_atomic env t;

 term2str s;

 term2str s;

 val t = str2term 

 val t = str2term 

 "dropWhile (ident (A = a * b))\

 "dropWhile (ident (A = a * b))\

 \ [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";

 \ [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";

 val s' = term2str t';

 val s' = term2str t';

 if s' = "[a / 2 = r * sin alpha, b / 2 = r * cos alpha]" 

 if s' = "[a / 2 = r * sin alpha, b / 2 = r * cos alpha]" 

 then () else raise error "new behaviour with list_rls 3.2.";

 then () else raise error "new behaviour with list_rls 3.2.";

 val env = env @ [(str2term "es_::bool list", str2term s')];

 val env = env @ [(str2term "es_::bool list", str2term s')];

 (*--- 3.line in script ---*)

 (*--- 3.line in script ---*)

 val t = str2term "dropWhile (ident (f_::real)) (Vars (h_::bool))";

 val t = str2term "dropWhile (ident (f_::real)) (Vars (h_::bool))";

 val s = subst_atomic env t;

 val s = subst_atomic env t;

 term2str s;

 term2str s;

 val t = str2term "dropWhile (ident A) (Vars (A = a * b))";

 val t = str2term "dropWhile (ident A) (Vars (A = a * b))";

 val s' = term2str t';

 val s' = term2str t';

 if s' = "[a, b]" then () else raise error "new behaviour with list_rls 3.3.";

 if s' = "[a, b]" then () else raise error "new behaviour with list_rls 3.3.";

 val env = env @ [(str2term "vs_::real list", str2term s')];

 val env = env @ [(str2term "vs_::real list", str2term s')];

 (*--- 4.line in script ---*)

 (*--- 4.line in script ---*)

 val t = str2term "nth_ 1 vs_";

 val t = str2term "nth_ 1 vs_";

 val s = subst_atomic env t;

 val s = subst_atomic env t;

 term2str s;

 term2str s;

 val t = str2term "nth_ 1 [a, b]";

 val t = str2term "nth_ 1 [a, b]";

 val s' = term2str t';

 val s' = term2str t';

 if s' = "a" then () else raise error "new behaviour with list_rls 3.4.";

 if s' = "a" then () else raise error "new behaviour with list_rls 3.4.";

 val env = env @ [(str2term "v_1", str2term s')];

 val env = env @ [(str2term "v_1", str2term s')];

 (*--- 5.line in script ---*)

 (*--- 5.line in script ---*)

 val t = str2term "nth_ 2 vs_";

 val t = str2term "nth_ 2 vs_";

 val s = subst_atomic env t;

 val s = subst_atomic env t;

 term2str s;

 term2str s;

 val t = str2term "nth_ 2 [a, b]";

 val t = str2term "nth_ 2 [a, b]";

 val s' = term2str t';

 val s' = term2str t';

 if s' = "b" then () else raise error "new behaviour with list_rls 3.5.";

 if s' = "b" then () else raise error "new behaviour with list_rls 3.5.";

 val env = env @ [(str2term "v_2", str2term s')];

 val env = env @ [(str2term "v_2", str2term s')];

 (*--- 6.line in script ---*)

 (*--- 6.line in script ---*)

 val t = str2term "(hd o (filterVar v_1)) (es_::bool list)";

 val t = str2term "(hd o (filterVar v_1)) (es_::bool list)";

 val s = subst_atomic env t;

 val s = subst_atomic env t;

 term2str s;

 term2str s;

 val t = str2term 

 val t = str2term 

 	   "(hd o filterVar a) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";

 	   "(hd o filterVar a) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";

 val s' = term2str t';

 val s' = term2str t';

 if s' = "a / 2 = r * sin alpha" then () 

 if s' = "a / 2 = r * sin alpha" then () 

 else raise error "new behaviour with list_rls 3.6.";

 else raise error "new behaviour with list_rls 3.6.";

 val e_1 = str2term "e_1::bool";

 val e_1 = str2term "e_1::bool";

 val env = env @ [(e_1, str2term s')];

 val env = env @ [(e_1, str2term s')];

 val t = str2term "(hd o (filterVar v_2)) (es_::bool list)";

 val t = str2term "(hd o (filterVar v_2)) (es_::bool list)";

 val s = subst_atomic env t;

 val s = subst_atomic env t;

 term2str s;

 term2str s;

 val t = str2term 

 val t = str2term 

 	  "(hd o filterVar b) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";

 	  "(hd o filterVar b) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";

 val s' = term2str t';

 val s' = term2str t';

 if s' = "b / 2 = r * cos alpha" then () 

 if s' = "b / 2 = r * cos alpha" then () 

 else raise error "new behaviour with list_rls 3.7.";

 else raise error "new behaviour with list_rls 3.7.";

 val env = env @ [(str2term "e_2::bool", str2term s')];

 val env = env @ [(str2term "e_2::bool", str2term s')];

 "Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] (h_::bool)";

 "Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] (h_::bool)";

 val s = subst_atomic env t;

 val s = subst_atomic env t;

 term2str s;

 term2str s;

 "Substitute\n [(a = (rhs o hd) [a = 2 * r * sin alpha]),\

 "Substitute\n [(a = (rhs o hd) [a = 2 * r * sin alpha]),\

 \              (b = (rhs o hd) [b = 2 * r * cos alpha])] (A = a * b)";

 \              (b = (rhs o hd) [b = 2 * r * cos alpha])] (A = a * b)";

 val s'' = term2str s';

 val s'' = term2str s';

 if s'' = 

 if s'' = 

 "Substitute [a = 2 * r * sin alpha, b = 2 * r * cos alpha] (A = a * b)"

 "Substitute [a = 2 * r * sin alpha, b = 2 * r * cos alpha] (A = a * b)"

 then () else raise error "new behaviour with list_rls 3.10.";

 then () else raise error "new behaviour with list_rls 3.10.";