1.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy	Tue Feb 06 15:26:05 2018 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy	Tue Feb 06 16:18:43 2018 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4    the internal representation of "a + b * 3". The '...' indicate that some 
     1.5    details are still hidden; further details are received this way:
     1.6  *}
     1.7 -ML {* default_print_depth 99; @{term "a + b * 9"}; default_print_depth 5;
     1.8 +ML {* (*default_print_depth 99;*) @{term "a + b * 9"}; (*default_print_depth 5;*)
     1.9  *}
    1.10  text {* The internal representation is too comprehensive for several kinds of 
    1.11    inspection. Thus ISAC provides additional features, as we see below. First 
    1.12 @@ -113,7 +113,7 @@
    1.13    For instance, in the theory 'HOL' (short for high order logic) even more basic knowledge is 
    1.14    defined ('=' etc), but not yet '+' and '*', so you get 'NONE':
    1.15  *}
    1.16 -ML {*  parse @{theory "HOL"} "a + b * 3";
    1.17 +ML {*  parse @{theory "HOL.HOL"} "a + b * 3";
    1.18  *}
    1.19  text {* ISAC uses comparatively few definitions and theorems from Isabelle, see 
    1.20    \begin{itemize}

     2.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Tue Feb 06 15:26:05 2018 +0100
     2.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Tue Feb 06 16:18:43 2018 +0100
     2.3 @@ -33,7 +33,7 @@
     2.4  
     2.5    Please, skip this introductory ML-section in the first go ...*}
     2.6  ML {*
     2.7 -default_print_depth 1;
     2.8 +(*default_print_depth 1;*)
     2.9  val (thy, ro, er, inst) = 
    2.10      (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
    2.11  *}

     3.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy	Tue Feb 06 15:26:05 2018 +0100
     3.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy	Tue Feb 06 16:18:43 2018 +0100
     3.3 @@ -112,12 +112,12 @@
     3.4    Please, note only 'nxt' close to the beginning of the output and the resulting
     3.5    term at the end:
     3.6  *}
     3.7 -ML {* default_print_depth 40; *}
     3.8 +text {* default_print_depth 40; *}
     3.9  ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
    3.10  ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
    3.11  ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
    3.12  ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
    3.13 -ML {* default_print_depth 3; *}
    3.14 +text {* default_print_depth 3; *}
    3.15  text{* And, please, note that the result of applying the 'nxt' ruleset is to be
    3.16    found in the output of the next step !
    3.17  *}

     4.1 --- a/test/Tools/isac/Frontend/use-cases.sml	Tue Feb 06 15:26:05 2018 +0100
     4.2 +++ b/test/Tools/isac/Frontend/use-cases.sml	Tue Feb 06 16:18:43 2018 +0100
     4.3 @@ -347,7 +347,7 @@
     4.4   autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
     4.5   autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
     4.6   (*------------------------------------*)
     4.7 -(* default_print_depth 13; get_calc 1;
     4.8 +(* (*default_print_depth 13*) get_calc 1;
     4.9     *)
    4.10   autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
    4.11   (*calc-head of subproblem*)
    4.12 @@ -1285,7 +1285,7 @@
    4.13   if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else 
    4.14   error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
    4.15  (* for getting the list in whole length ...
    4.16 -default_print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);default_print_depth 3;
    4.17 +(*default_print_depth 99*) map fst (get_interval ([1],Res) ([],Res) 9999 pt); (*default_print_depth 3*)
    4.18     *)
    4.19   if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = 
    4.20      [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),

     5.1 --- a/test/Tools/isac/Interpret/calchead.sml	Tue Feb 06 15:26:05 2018 +0100
     5.2 +++ b/test/Tools/isac/Interpret/calchead.sml	Tue Feb 06 16:18:43 2018 +0100
     5.3 @@ -44,14 +44,14 @@
     5.4   val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
     5.5   val ((pt,_),_) = get_calc 1;
     5.6  
     5.7 -default_print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);default_print_depth 3;
     5.8 +(*default_print_depth 99*)map fst (get_interval ([],Pbl) ([],Res) 9999 pt);(*default_print_depth 3*)
     5.9  if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) = 
    5.10      [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), 
    5.11       ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
    5.12        ([3, 2], Res)] then () else
    5.13  error "calchead.sml: diff.behav. get_interval after replace} other 2 a";
    5.14  
    5.15 -default_print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); default_print_depth 3;
    5.16 +(*default_print_depth 99*)map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); (*default_print_depth 3*)
    5.17  if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) = 
    5.18      [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
    5.19  error "modspec.sml: diff.behav. get_interval after replace} other 2 b";

     6.1 --- a/test/Tools/isac/Interpret/ctree.sml	Tue Feb 06 15:26:05 2018 +0100
     6.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Tue Feb 06 16:18:43 2018 +0100
     6.3 @@ -211,7 +211,7 @@
     6.4  "-------------- cut_level (from ctree above)----------------------";
     6.5  show_pt pt;
     6.6  show_pt pt';
     6.7 -default_print_depth 99; cuts; default_print_depth 3;
     6.8 +(*default_print_depth 99*) cuts; (*default_print_depth 3*)
     6.9  
    6.10  (*if cuts = [([2], Res),
    6.11  	   ([3], Frm),
    6.12 @@ -377,8 +377,8 @@
    6.13  
    6.14  show_pt pt;
    6.15  show_pt pt';
    6.16 -default_print_depth 99;cuts;default_print_depth 3;
    6.17 -default_print_depth 99;map fst (get_interval ([],Frm) ([],Res) 9999 pt');default_print_depth 3;
    6.18 +(*default_print_depth 99;*)cuts;(*default_print_depth 3;*)
    6.19 +(*default_print_depth 99;*)map fst (get_interval ([],Frm) ([],Res) 9999 pt');(*default_print_depth 3;*)
    6.20  ####################################################################*)
    6.21  
    6.22  
    6.23 @@ -1039,9 +1039,9 @@
    6.24  "-------------- get_allpos' new ----------------------------------";
    6.25  "-------------- get_allpos' new ----------------------------------";
    6.26  "--- whole ctree";
    6.27 -default_print_depth 99;
    6.28 +(*default_print_depth 99;*)
    6.29  val cuts = get_allp [] ([], ([],Frm)) pt;
    6.30 -default_print_depth 3;
    6.31 +(*default_print_depth 3;*)
    6.32  if cuts = 
    6.33     [(*never returns the first pos'*)
    6.34      ([1], Frm), 
    6.35 @@ -1058,9 +1058,9 @@
    6.36      ([], Res)] then () else
    6.37  error "ctree.sml diff.behav. get_allp new []";
    6.38  
    6.39 -default_print_depth 99;
    6.40 +(*default_print_depth 99;*)
    6.41  val cuts2 = get_allps [] [1] (children pt);
    6.42 -default_print_depth 3;
    6.43 +(*default_print_depth 3;*)
    6.44  if cuts = cuts2 @ [([], Res)] then () else
    6.45  error "ctree.sml diff.behav. get_allps new []";
    6.46  
    6.47 @@ -1130,9 +1130,9 @@
    6.48  
    6.49  "---(2) on S(606)..S(608)--------";
    6.50  val (pt', cuts) = cut_tree pt ([1],Res);
    6.51 -default_print_depth 99;
    6.52 +(*default_print_depth 99;*)
    6.53  cuts;
    6.54 -default_print_depth 3;
    6.55 +(*default_print_depth 3;*)
    6.56  if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
    6.57        ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
    6.58        ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
    6.59 @@ -1143,9 +1143,9 @@
    6.60  
    6.61  "---(3) on S(606)..S(608)--------";
    6.62  val (pt', cuts) = cut_tree pt ([2],Res);
    6.63 -default_print_depth 99;
    6.64 +(*default_print_depth 99;*)
    6.65  cuts;
    6.66 -default_print_depth 3;
    6.67 +(*default_print_depth 3;*)
    6.68  if cuts = [(*preceding step on WS was ([1]),Res*)
    6.69  	   ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
    6.70  	   ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), 
    6.71 @@ -1162,9 +1162,9 @@
    6.72  
    6.73  "---(4) on S(606)..S(608)--------";
    6.74  val (pt', cuts) = cut_tree pt ([3],Pbl);
    6.75 -default_print_depth 99;
    6.76 +(*default_print_depth 99;*)
    6.77  cuts;
    6.78 -default_print_depth 3;
    6.79 +(*default_print_depth 3;*)
    6.80  if cuts = [([3], Pbl),
    6.81  	   ([3, 1], Frm), ([3, 1], Res), 
    6.82  	   ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
    6.83 @@ -1176,7 +1176,7 @@
    6.84  
    6.85  "---(5a) on S(606)..S(608) cut_tree --------";
    6.86  val (pt', cuts) = cut_tree pt ([3,2,1],Res);
    6.87 -default_print_depth 99;
    6.88 +(*default_print_depth 99;*)
    6.89  cuts;
    6.90  default_print_depth 1;
    6.91  if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),([],Res)] then () 
    6.92 @@ -1195,9 +1195,9 @@
    6.93  val (pt', cuts) = cappend_atomic pt [1] e_istate (str2term "Inform[1]")
    6.94      (Tac "test") (str2term "Inres[1]",[]) Complete;
    6.95  
    6.96 -default_print_depth 99;
    6.97 +(*default_print_depth 99;*)
    6.98  cuts;
    6.99 -default_print_depth 3;
   6.100 +(*default_print_depth 3;*)
   6.101  if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
   6.102        ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
   6.103        ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
   6.104 @@ -1206,9 +1206,9 @@
   6.105  else error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
   6.106  
   6.107  val afterins = get_allp [] ([], ([],Frm)) pt';
   6.108 -default_print_depth 99;
   6.109 +(*default_print_depth 99;*)
   6.110  afterins;
   6.111 -default_print_depth 3;
   6.112 +(*default_print_depth 3;*)
   6.113  if afterins = [([1], Frm), ([1], Res)] then()
   6.114  else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
   6.115  show_pt pt';
   6.116 @@ -1216,9 +1216,9 @@
   6.117  show_pt pt;
   6.118  val (pt', cuts) = cappend_atomic pt [2] e_istate (str2term "Inform[2]")
   6.119      (Tac "test") (str2term "Inres[2]",[]) Complete;
   6.120 -default_print_depth 99;
   6.121 +(*default_print_depth 99;*)
   6.122  cuts;
   6.123 -default_print_depth 3;
   6.124 +(*default_print_depth 3;*)
   6.125  
   6.126  if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
   6.127        ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl), 
   6.128 @@ -1229,9 +1229,9 @@
   6.129  
   6.130  
   6.131  val afterins = get_allp [] ([], ([],Frm)) pt';
   6.132 -default_print_depth 99;
   6.133 +(*default_print_depth 99;*)
   6.134  afterins;
   6.135 -default_print_depth 3;
   6.136 +(*default_print_depth 3;*)
   6.137  
   6.138  if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)] 
   6.139  then () else
   6.140 @@ -1253,9 +1253,9 @@
   6.141  "---(4) on S(606)..S(608)--------";
   6.142  val (pt', cuts) = cappend_problem pt [3] e_istate ([],e_spec)
   6.143  				  ([],e_spec, str2term "Inhead[3]");
   6.144 -default_print_depth 99;
   6.145 +(*default_print_depth 99;*)
   6.146  cuts;
   6.147 -default_print_depth 3;
   6.148 +(*default_print_depth 3;*)
   6.149  if cuts = [([3], Pbl),
   6.150  	   ([3, 1], Frm), ([3, 1], Res), 
   6.151  	   ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
   6.152 @@ -1264,9 +1264,9 @@
   6.153  	   ([], Res)] then ()else
   6.154  error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
   6.155  val afterins = get_allp [] ([], ([],Frm)) pt';
   6.156 -default_print_depth 99;
   6.157 +(*default_print_depth 99;*)
   6.158  afterins;
   6.159 -default_print_depth 3;
   6.160 +(*default_print_depth 3;*)
   6.161  if afterins = 
   6.162     [([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
   6.163      ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res),
   6.164 @@ -1279,18 +1279,18 @@
   6.165  "---(6-1) on S(606)..S(608)--------";
   6.166  val (pt', cuts) = cappend_atomic pt [3,1] e_istate (str2term "Inform[3,1]")
   6.167      (Tac "test") (str2term "Inres[3,1]",[]) Complete;
   6.168 -default_print_depth 99;
   6.169 +(*default_print_depth 99;*)
   6.170  cuts;
   6.171 -default_print_depth 3;
   6.172 +(*default_print_depth 3;*)
   6.173  if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
   6.174  	   ([3, 2], Res),
   6.175  (*WN060727 added*)([3], Res), ([4], Res), ([], Res)] then () else
   6.176  error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
   6.177  
   6.178  val afterins = get_allp [] ([], ([],Frm)) pt';
   6.179 -default_print_depth 99;
   6.180 +(*default_print_depth 99;*)
   6.181  afterins;
   6.182 -default_print_depth 3;
   6.183 +(*default_print_depth 3;*)
   6.184  if afterins = [([1], Frm), ([1], Res), 
   6.185  	       ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
   6.186  	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), 
   6.187 @@ -1305,15 +1305,15 @@
   6.188  "---(6) on S(606)..S(608)--------";
   6.189  val (pt', cuts) = cappend_atomic pt [3,2] e_istate (str2term "Inform[3,2]")
   6.190      (Tac "test") (str2term "Inres[3,2]",[]) Complete;
   6.191 -default_print_depth 99;
   6.192 +(*default_print_depth 99;*)
   6.193  cuts;
   6.194 -default_print_depth 3;
   6.195 +(*default_print_depth 3;*)
   6.196  if cuts = [([3], Res), ([4], Res), ([], Res)] then () else
   6.197  error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
   6.198  val afterins = get_allp [] ([], ([],Frm)) pt';
   6.199 -default_print_depth 99;
   6.200 +(*default_print_depth 99;*)
   6.201  afterins;
   6.202 -default_print_depth 3;
   6.203 +(*default_print_depth 3;*)
   6.204  if afterins = [([1], Frm), ([1], Res), 
   6.205  	       ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
   6.206  	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), 
   6.207 @@ -1330,16 +1330,16 @@
   6.208  (**)
   6.209  val (pt', cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "Inform[3,2,1]")
   6.210      (Tac "test") (str2term "Inres[3,2,1]",[]) Complete;
   6.211 -default_print_depth 99;
   6.212 +(*default_print_depth 99;*)
   6.213  cuts;
   6.214  default_print_depth 1;
   6.215  if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)] 
   6.216  then () else
   6.217  error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
   6.218  val afterins = get_allp [] ([], ([],Frm)) pt';
   6.219 -default_print_depth 99;
   6.220 +(*default_print_depth 99;*)
   6.221  afterins;
   6.222 -default_print_depth 3;
   6.223 +(*default_print_depth 3;*)
   6.224  if afterins = [([1], Frm), ([1], Res), 
   6.225  	       ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
   6.226  	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), 

     7.1 --- a/test/Tools/isac/Interpret/inform.sml	Tue Feb 06 15:26:05 2018 +0100
     7.2 +++ b/test/Tools/isac/Interpret/inform.sml	Tue Feb 06 16:18:43 2018 +0100
     7.3 @@ -642,7 +642,7 @@
     7.4  val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
     7.5  val NONE = env;
     7.6  val (SOME istate, NONE) = loc;
     7.7 -default_print_depth 5;
     7.8 +(*default_print_depth 5;*)
     7.9  writeln"-----------------------------------------------------------";
    7.10  spec;
    7.11  writeln (itms2str_ ctxt probl);
    7.12 @@ -660,11 +660,11 @@
    7.13  val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
    7.14  val NONE = env;
    7.15  val (SOME istate, NONE) = loc;
    7.16 -default_print_depth 5; writeln (istate2str (fst istate));  default_print_depth 3;
    7.17 +(*default_print_depth 5;*) writeln (istate2str (fst istate));  (*default_print_depth 3;*)
    7.18  (*ScrState ([],
    7.19   [], NONE,
    7.20   ??.empty, Sundef, false)*)
    7.21 -default_print_depth 5; spec; default_print_depth 3;
    7.22 +(*default_print_depth 5;*) spec; (*default_print_depth 3;*)
    7.23  (*("Isac",
    7.24        ["derivative_of", "function"],
    7.25        ["diff", "differentiate_on_R"]) : spec*)
    7.26 @@ -704,11 +704,11 @@
    7.27  val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
    7.28  val NONE = env;
    7.29  val (SOME istate, NONE) = loc;
    7.30 -default_print_depth 5; writeln (istate2str (fst istate));  default_print_depth 3;
    7.31 +(*default_print_depth 5;*) writeln (istate2str (fst istate));  (*default_print_depth 3;*)
    7.32  (*ScrState ([],
    7.33   [], NONE,
    7.34   ??.empty, Sundef, false)*)
    7.35 -default_print_depth 5; spec; default_print_depth 3;
    7.36 +(*default_print_depth 5;*) spec; (*default_print_depth 3;*)
    7.37  (*("Isac",
    7.38        ["derivative_of", "function"],
    7.39        ["diff", "differentiate_on_R"]) : spec*)

     8.1 --- a/test/Tools/isac/Interpret/rewtools.sml	Tue Feb 06 15:26:05 2018 +0100
     8.2 +++ b/test/Tools/isac/Interpret/rewtools.sml	Tue Feb 06 16:18:43 2018 +0100
     8.3 @@ -253,7 +253,7 @@
     8.4  "----------- fun guh2theID ------------------------------";
     8.5  "----------- fun guh2theID ------------------------------";
     8.6  val guh = "thy_scri_ListG-thm-zip_Nil";
     8.7 -default_print_depth 3; (*999*)
     8.8 +(*default_print_depth 3; 999*)
     8.9  take_fromto 1 4 (Symbol.explode guh);
    8.10  take_fromto 5 9 (Symbol.explode guh);
    8.11  val rest = takerest (9,(Symbol.explode guh)); 

     9.1 --- a/test/Tools/isac/Interpret/solve.sml	Tue Feb 06 15:26:05 2018 +0100
     9.2 +++ b/test/Tools/isac/Interpret/solve.sml	Tue Feb 06 16:18:43 2018 +0100
     9.3 @@ -9,7 +9,7 @@
     9.4  uses from Poly.ML: Rls make_polynomial, Rls expand_binom 
     9.5  *)
     9.6  
     9.7 -default_print_depth 5;
     9.8 +(*default_print_depth 5;*)
     9.9  trace_rewrite := false;
    9.10  trace_script := false;
    9.11  "-----------------------------------------------------------------";

    10.1 --- a/test/Tools/isac/Knowledge/atools.sml	Tue Feb 06 15:26:05 2018 +0100
    10.2 +++ b/test/Tools/isac/Knowledge/atools.sml	Tue Feb 06 16:18:43 2018 +0100
    10.3 @@ -7,7 +7,7 @@
    10.4  use"atools.sml";
    10.5  *)
    10.6  
    10.7 -default_print_depth 5;
    10.8 +(*default_print_depth 5;*)
    10.9  "--------------------------------------------------------";
   10.10  "table of contents --------------------------------------";
   10.11  "--------------------------------------------------------";

    11.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml	Tue Feb 06 15:26:05 2018 +0100
    11.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml	Tue Feb 06 16:18:43 2018 +0100
    11.3 @@ -42,17 +42,17 @@
    11.4      here     = {Pure, .., Inverse_Z_Transform, Isac, Test_Build_Thydata, Test_Theory:111}   *)
    11.5    val proglang_parent = @{theory ProgLang}
    11.6    val allthys = Theory.ancestors_of @{theory};
    11.7 -  val allthys = filter_out (member Theory.eq_thy (* thys for isac bootstrap *)
    11.8 +  val allthys = filter_out (member Context.eq_thy (* thys for isac bootstrap *)
    11.9      [(*@{theory ProgLang}: required in isacthys' below*) @{theory Interpret}, @{theory xmlsrc},
   11.10      @{theory Frontend}, knowledge_parent]) allthys         (*["Isac", ..., "Pure"]*)
   11.11    val isabthys' =                         (*["Complex_Main", "Taylor", .., "Pure"]*)
   11.12 -    drop ((find_index (curry Theory.eq_thy @{theory Complex_Main}) allthys), allthys);
   11.13 +    drop ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
   11.14    val isacthys' =                         (*["Isac", "Inverse_Z_Transform",  .., "KEStore"]*)
   11.15 -    take ((find_index (curry Theory.eq_thy @{theory Complex_Main}) allthys), allthys);
   11.16 +    take ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
   11.17    val knowthys' =                         (*["Isac", .., "Descript", "Delete"]*)
   11.18 -    take ((find_index (curry Theory.eq_thy proglang_parent) isacthys'), isacthys');
   11.19 +    take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys');
   11.20    val progthys' =                         (*["Script", "Tools", "ListC", "KEStore"]*)
   11.21 -    drop ((find_index (curry Theory.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys');
   11.22 +    drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys');
   11.23    val isacrlsthms =                      (*length = 460*)
   11.24      thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (thmID * thm) list
   11.25    val rlsthmsNOTisac = isacrlsthms       (*length =  36*)

    12.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml	Tue Feb 06 15:26:05 2018 +0100
    12.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml	Tue Feb 06 16:18:43 2018 +0100
    12.3 @@ -424,7 +424,7 @@
    12.4  trace_rewrite := false;
    12.5  val matches = refine fmz ["2x2", "LINEAR","system"];
    12.6  trace_rewrite:=false;
    12.7 -default_print_depth 11; matches; default_print_depth 3;
    12.8 +(*default_print_depth 11;*) matches; (*default_print_depth 3;*)
    12.9  (*brought: 'False "length_ es_ = 2"'*)
   12.10  
   12.11  (*-----fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) =

    13.1 --- a/test/Tools/isac/Knowledge/gcd_poly_winkler.sml	Tue Feb 06 15:26:05 2018 +0100
    13.2 +++ b/test/Tools/isac/Knowledge/gcd_poly_winkler.sml	Tue Feb 06 16:18:43 2018 +0100
    13.3 @@ -86,7 +86,7 @@
    13.4    doe not conform with the Isabelle coding standards)
    13.5  *}*)
    13.6  
    13.7 - default_print_depth 3; (*20*)
    13.8 + (*default_print_depth 3; 20*)
    13.9   type unipoly = int list;
   13.10  
   13.11  "----------- auxiliary functions univariate -------------";

    14.1 --- a/test/Tools/isac/Knowledge/poly.sml	Tue Feb 06 15:26:05 2018 +0100
    14.2 +++ b/test/Tools/isac/Knowledge/poly.sml	Tue Feb 06 16:18:43 2018 +0100
    14.3 @@ -376,9 +376,9 @@
    14.4  (*...if there is an error, then ...*)
    14.5  
    14.6  "-----1 ---";
    14.7 -default_print_depth 7;
    14.8 +(*default_print_depth 7;*)
    14.9  val pbt = get_pbt ["polynomial","simplification"];
   14.10 -default_print_depth 3;
   14.11 +(*default_print_depth 3;*)
   14.12  (*if there is ...
   14.13  > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
   14.14  ... then trace_rewrite:*)
   14.15 @@ -390,9 +390,9 @@
   14.16  (*... if there is no rewrite, then there is something wrong with prls*)
   14.17                                
   14.18  "-----3 ---";
   14.19 -default_print_depth 7;
   14.20 +(*default_print_depth 7;*)
   14.21  val prls = (#prls o get_pbt) ["polynomial","simplification"];
   14.22 -default_print_depth 3;
   14.23 +(*default_print_depth 3;*)
   14.24  val t = str2term "((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)) is_polyexp";
   14.25  val SOME (t',_) = rewrite_set_ thy false prls t;
   14.26  if t' = @{term True} then () 

    15.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Tue Feb 06 15:26:05 2018 +0100
    15.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Tue Feb 06 16:18:43 2018 +0100
    15.3 @@ -550,9 +550,9 @@
    15.4  "----------- refine Vereinfache ----------------------------------";
    15.5  "----------- refine Vereinfache ----------------------------------";
    15.6  val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*(q::real)))", "normalform (N::real)"];
    15.7 -default_print_depth 11;
    15.8 +(*default_print_depth 11;*)
    15.9  val matches = refine fmz ["vereinfachen"];
   15.10 -default_print_depth 3;
   15.11 +(*default_print_depth 3;*)
   15.12  
   15.13  "----- go into details, if it seems not to work -----";
   15.14  "--- does the predicate evaluate correctly ?";

    16.1 --- a/test/Tools/isac/Knowledge/rational.sml	Tue Feb 06 15:26:05 2018 +0100
    16.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Tue Feb 06 16:18:43 2018 +0100
    16.3 @@ -350,9 +350,9 @@
    16.4          val vs = t |> vars |> map free2str |> sort string_ord
    16.5          val baseT = type_of numerator
    16.6          val expT = HOLogic.realT;
    16.7 -default_print_depth 3; (*999*)
    16.8 +(*default_print_depth 3; 999*)
    16.9  val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator);
   16.10 -default_print_depth 3; (*999*)
   16.11 +(*default_print_depth 3; 999*)
   16.12  (* does not terminate instead of returning ?:
   16.13          val ((a', b'), c) = gcd_poly a b
   16.14  val a = [(~12, [0, 0]), (3, [2, 0]), (4, [0, 1]), (~1, [2, 1])]: poly
   16.15 @@ -413,10 +413,10 @@
   16.16  term2str n1; term2str d1; term2str n2; term2str d2;
   16.17        val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *)
   16.18          |> filter is_some |> map the |> sort string_ord;
   16.19 -default_print_depth 3; (*999*)
   16.20 +(*default_print_depth 3; 999*)
   16.21  val (SOME _, SOME a, SOME _, SOME b) =
   16.22    (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2);
   16.23 -default_print_depth 3; (*999*)
   16.24 +(*default_print_depth 3; 999*)
   16.25  (*
   16.26  val a = [(1, [1, 0, 0]), (~1, [0, 1, 1])]: poly
   16.27  val b = [(1, [1, 0, 0]), (1, [0, 1, 1])]: poly
   16.28 @@ -1581,22 +1581,22 @@
   16.29  val {rules, rew_ord= (_, ro), ...} = rep_rls (assoc_rls "rev_rew_p");
   16.30  val der = make_deriv thy Atools_erls rules ro NONE tt;
   16.31  if length der = 12 then () else error "WN1130912 rls chancel_p 4";
   16.32 -default_print_depth 99; writeln (deriv2str der); default_print_depth 3;
   16.33 +(*default_print_depth 99;*) writeln (deriv2str der); (*default_print_depth 3;*)
   16.34  
   16.35 -default_print_depth 99; map (term2str o #1) der; default_print_depth 3;
   16.36 +(*default_print_depth 99;*) map (term2str o #1) der; (*default_print_depth 3;*)
   16.37  "...,(-1 * b ^^^ 2 + a ^^^ 2) / (-2 * (a * b) + a ^^^ 2 + (-1 * b) ^^^ 2) ]";
   16.38 -default_print_depth 99; map (rule2str o #2) der; default_print_depth 3;
   16.39 -default_print_depth 99; map (term2str o #1 o #3) der; default_print_depth 3;
   16.40 +(*default_print_depth 99;*) map (rule2str o #2) der; (*default_print_depth 3;*)
   16.41 +(*default_print_depth 99;*) map (term2str o #1 o #3) der; (*default_print_depth 3;*)
   16.42  
   16.43  val der = make_deriv thy Atools_erls rules ro NONE 
   16.44  	(str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");
   16.45 -default_print_depth 99; writeln (deriv2str der); default_print_depth 3;
   16.46 +(*default_print_depth 99;*) writeln (deriv2str der); (*default_print_depth 3;*)
   16.47  
   16.48  val {rules, rew_ord=(_,ro),...} = rep_rls (assoc_rls "rev_rew_p");
   16.49  val der = make_deriv thy Atools_erls rules ro NONE 
   16.50  	(str2term "(1 * a + -1 * b) * (1 * a + -1 * b)");
   16.51 -default_print_depth 99; writeln (deriv2str der); default_print_depth 3;
   16.52 -default_print_depth 99; map (term2str o #1) der; default_print_depth 3;
   16.53 +(*default_print_depth 99;*) writeln (deriv2str der); (*default_print_depth 3;*)
   16.54 +(*default_print_depth 99;*) map (term2str o #1) der; (*default_print_depth 3;*)
   16.55  (*WN060829 ...postponed*)
   16.56  
   16.57  

    17.1 --- a/test/Tools/isac/OLDTESTS/modspec.sml	Tue Feb 06 15:26:05 2018 +0100
    17.2 +++ b/test/Tools/isac/OLDTESTS/modspec.sml	Tue Feb 06 16:18:43 2018 +0100
    17.3 @@ -24,14 +24,14 @@
    17.4   val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
    17.5   val ((pt,_),_) = get_calc 1;
    17.6  
    17.7 -default_print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);default_print_depth 3;
    17.8 +(*default_print_depth 99;*)map fst (get_interval ([],Pbl) ([],Res) 9999 pt);(*default_print_depth 3;*)
    17.9  if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) = 
   17.10      [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), 
   17.11       ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
   17.12        ([3, 2], Res)] then () else
   17.13  error "modspec.sml: diff.behav. get_interval after replace} other 2 a";
   17.14  
   17.15 -default_print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); default_print_depth 3;
   17.16 +(*default_print_depth 99;*)map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); (*default_print_depth 3;*)
   17.17  if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) = 
   17.18      [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
   17.19  error "modspec.sml: diff.behav. get_interval after replace} other 2 b";

    18.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Tue Feb 06 15:26:05 2018 +0100
    18.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Tue Feb 06 16:18:43 2018 +0100
    18.3 @@ -502,7 +502,7 @@
    18.4  "----------- 2011 thms with axclasses -------------------";
    18.5  "----------- 2011 thms with axclasses -------------------";
    18.6  "----------- 2011 thms with axclasses -------------------";
    18.7 -val thm = num_str @{thm divide_1};
    18.8 +val thm = num_str @{thm div_by_1};
    18.9  val prop = Thm.prop_of thm;
   18.10  atomty prop;                                     (*Type 'a*)
   18.11  val t = str2term "(2*x)/1";                      (*Type real*)

    19.1 --- a/test/Tools/isac/ProgLang/termC.sml	Tue Feb 06 15:26:05 2018 +0100
    19.2 +++ b/test/Tools/isac/ProgLang/termC.sml	Tue Feb 06 16:18:43 2018 +0100
    19.3 @@ -183,7 +183,7 @@
    19.4    "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n==>" ^
    19.5    " (?a + ?b = ?c) = (?b = ?c + -1 * ?a)"
    19.6  then () else error "termC.sml separate_bdvs_add";
    19.7 -default_print_depth 5; 
    19.8 +(*default_print_depth 5;*)
    19.9  
   19.10  val subst = 
   19.11    [(str2term "bdv_1", str2term "c"),
   19.12 @@ -222,7 +222,7 @@
   19.13   val pat = (free2var o Thm.term_of o the o (parse thy)) "a * b^^^2 = (c::real)";
   19.14   (*        !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*)
   19.15   val insts = Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty);
   19.16 -default_print_depth 3; (*999*) insts; 
   19.17 +(*default_print_depth 3; 999*) insts; 
   19.18   (*val insts =
   19.19     ({}, 
   19.20      {(("a", 0), ("Real.real", Free ("3", "Real.real"))), 
   19.21 @@ -443,9 +443,9 @@
   19.22   writeln "----------------SAME output: no markup----";
   19.23  
   19.24   writeln "----------------writeln PolyML.makestring str_markup---";
   19.25 - writeln (PolyML.makestring str_markup);
   19.26 + writeln (@{make_string} str_markup);
   19.27   writeln "----------------writeln PolyML.makestring str---";
   19.28 - writeln (PolyML.makestring str);
   19.29 + writeln (@{make_string} str);
   19.30   writeln "----------------DIFFERENT output----";
   19.31  
   19.32   tracing "----------------tracing str_markup---";
   19.33 @@ -455,9 +455,9 @@
   19.34   tracing "----------------SAME output: no markup----";
   19.35  
   19.36   tracing "----------------writeln PolyML.makestring str_markup---";
   19.37 - tracing (PolyML.makestring str_markup);
   19.38 + tracing (@{make_string} str_markup);
   19.39   tracing "----------------writeln PolyML.makestring str---";
   19.40 - tracing (PolyML.makestring str);
   19.41 + tracing (@{make_string} str);
   19.42   tracing "----------------DIFFERENT output----";
   19.43  (*
   19.44   redirect_tracing "../../tmp/";
   19.45 @@ -481,9 +481,9 @@
   19.46   writeln "----------------SAME output: no markup----";
   19.47  
   19.48   writeln "----------------writeln PolyML.makestring str_markup---";
   19.49 - writeln (PolyML.makestring str_markup);
   19.50 + writeln (@{make_string} str_markup);
   19.51   writeln "----------------writeln PolyML.makestring str---";
   19.52 - writeln (PolyML.makestring str);
   19.53 + writeln (@{make_string} str);
   19.54   writeln "----------------DIFFERENT output----";
   19.55  
   19.56   tracing "----------------tracing str_markup---";
   19.57 @@ -493,9 +493,9 @@
   19.58   tracing "----------------SAME output: no markup----";
   19.59  
   19.60   tracing "----------------writeln PolyML.makestring str_markup---";
   19.61 - tracing (PolyML.makestring str_markup);
   19.62 + tracing (@{make_string} str_markup);
   19.63   tracing "----------------writeln PolyML.makestring str---";
   19.64 - tracing (PolyML.makestring str);
   19.65 + tracing (@{make_string} str);
   19.66   tracing "----------------DIFFERENT output----";
   19.67  (*
   19.68   redirect_tracing "../../tmp/";

    20.1 --- a/test/Tools/isac/calcelems.sml	Tue Feb 06 15:26:05 2018 +0100
    20.2 +++ b/test/Tools/isac/calcelems.sml	Tue Feb 06 16:18:43 2018 +0100
    20.3 @@ -74,7 +74,7 @@
    20.4  pretty types:
    20.5   PolyML.addPrettyPrinter
    20.6     (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
    20.7 - default_print_depth 3;
    20.8 + (*default_print_depth 3;*)
    20.9  *)
   20.10  "===== extend parse to string with markup===";
   20.11  (*

    21.1 --- a/test/Tools/isac/xmlsrc/datatypes.sml	Tue Feb 06 15:26:05 2018 +0100
    21.2 +++ b/test/Tools/isac/xmlsrc/datatypes.sml	Tue Feb 06 16:18:43 2018 +0100
    21.3 @@ -37,7 +37,7 @@
    21.4  "~~~~~ fun get_the, args:"; val (theID:theID) = (["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]);
    21.5  (*get_py  (Thy_Info.get_theory "Pure") theID theID (get_thes ()); 
    21.6    (* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
    21.7 -default_print_depth 3; (*999*)
    21.8 +(*default_print_depth 3; 999*)
    21.9  (get_thes ());
   21.10  
   21.11  (*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((Thy_Info.get_theory "Pure"), theID, theID, (get_thes ()));*)