1.1 --- a/etc/settings	Mon Apr 20 10:33:55 2015 +0200
     1.2 +++ b/etc/settings	Mon Apr 20 14:18:40 2015 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  
     1.5  # The place for user configuration, heap files, etc.
     1.6  if [ -z "$ISABELLE_IDENTIFIER" ]; then
     1.7 -  ISABELLE_HOME_USER="$USER_HOME/.isabelle"
     1.8 +  ISABELLE_HOME_USER="$USER_HOME/.isabelle/isabisac"
     1.9  else
    1.10    ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER"
    1.11  fi

     2.1 --- a/src/Pure/ROOT.ML	Mon Apr 20 10:33:55 2015 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Mon Apr 20 14:18:40 2015 +0200
     2.3 @@ -4,8 +4,8 @@
     2.4  
     2.5  structure Distribution =     (*filled-in by makedist*)
     2.6  struct
     2.7 -  val version = "repository version: Isabelle2014: August 2014 + Isabelle/Isac";
     2.8 -  val is_identified = true;
     2.9 +  val version = "Isabelle2014: August 2014 + Isabelle/Isac";
    2.10 +  val is_identified = false;
    2.11    val is_official = false;
    2.12  end;
    2.13  

     3.1 --- a/src/Pure/ROOT.scala	Mon Apr 20 10:33:55 2015 +0200
     3.2 +++ b/src/Pure/ROOT.scala	Mon Apr 20 14:18:40 2015 +0200
     3.3 @@ -9,8 +9,8 @@
     3.4  {
     3.5    object Distribution     /*filled-in by makedist*/
     3.6    {
     3.7 -    val version = "repository version: Isabelle2014: August 2014 + Isabelle/Isac"
     3.8 -    val is_identified = true
     3.9 +    val version = "Isabelle2014: August 2014 + Isabelle/Isac"
    3.10 +    val is_identified = false
    3.11      val is_official = false
    3.12    }
    3.13  }

     4.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_OLD.thy	Mon Apr 20 10:33:55 2015 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_OLD.thy	Mon Apr 20 14:18:40 2015 +0200
     4.3 @@ -67,18 +67,18 @@
     4.4  (* arguments from the example from [1].p.94 *)
     4.5  value "       primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" 
     4.6    --"= Poly [-2, -1, 1]  OK"
     4.7 -value [simp] "primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" 
     4.8 +value (*[simp]*) "primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" 
     4.9    --"= [:-2, -1, 1, 0:]  incorrect ???????????????????????????????????????????????????????????"
    4.10  (* goes forever:
    4.11 -value [nbe]  "primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" 
    4.12 +value (*[nbe]*)  "primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" 
    4.13  *)
    4.14 -value [code] "primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" 
    4.15 +value (*[code]*) "primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" 
    4.16    --"= Poly [-2, -1, 1] ...ok"
    4.17  
    4.18  (*where does [simp] fail:*)
    4.19 -value [simp] "let p = [:-5000595353600, -2500297676800, 2500297676800::int:] 
    4.20 +value (*[simp]*) "let p = [:-5000595353600, -2500297676800, 2500297676800::int:] 
    4.21  in (coeffs p)"       --{* = "[-5000595353600, -2500297676800, 2500297676800]" :: "int list" OK*}
    4.22 -value [simp] "let p = [:-5000595353600, -2500297676800, 2500297676800::int:] 
    4.23 +value (*[simp]*) "let p = [:-5000595353600, -2500297676800, 2500297676800::int:] 
    4.24  in gcds (coeffs p)"  --{* = "2500297676800" :: "int" OK*}
    4.25  (* declare [[simp_trace = true]]
    4.26  value [simp] "let p = [:-5000595353600, -2500297676800, 2500297676800::int:] 
    4.27 @@ -86,7 +86,7 @@
    4.28  ... gives an unreadable trace, unfortunately.*)
    4.29  
    4.30  (*where does  [nbe] fail:*)
    4.31 -value [nbe]  "let p = [:-5000595353600, -2500297676800, 2500297676800::int:] 
    4.32 +value (*[nbe]*)  "let p = [:-5000595353600, -2500297676800, 2500297676800::int:] 
    4.33  in (coeffs p)" --{* = "coeffs (Poly (-5000595353600 # coeffs (Poly (-2500297676800 # coef... ???*}
    4.34  (* value [nbe]  "let p = [:-5000595353600, -2500297676800, 2500297676800::int:] 
    4.35  in gcds (coeffs p)"
    4.36 @@ -193,10 +193,10 @@
    4.37    "euclidean_algorithm [:-18, -15, -20, 12, 20, -13, 2::int:]  [:8, 28, 22, -11, -14, 1, 2:]"
    4.38  value [simp]
    4.39    "euclidean_algorithm [:-18, -15, -20, 12, 20, -13, 2::int:]  [:8, 28, 22, -11, -14, 1, 2:]"*)
    4.40 -value [nbe] 
    4.41 +value (*[nbe]*)
    4.42    "euclidean_algorithm [:-18, -15, -20, 12, 20, -13, 2::int:]  [:8, 28, 22, -11, -14, 1, 2:]"
    4.43  (* = "euclidean_algorithm (Poly (-18 # coeffs (Poly (-15 # coeffs ...why not simplified ???*)
    4.44 -value [code]
    4.45 +value (*[code]*)
    4.46    "euclidean_algorithm [:-18, -15, -20, 12, 20, -13, 2::int:]  [:8, 28, 22, -11, -14, 1, 2:]"
    4.47  (* = "Poly [-2, -1, 1]"*)
    4.48  

     5.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy	Mon Apr 20 10:33:55 2015 +0200
     5.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy	Mon Apr 20 14:18:40 2015 +0200
     5.3 @@ -71,7 +71,7 @@
     5.4    the internal representation of "a + b * 3". The '...' indicate that some 
     5.5    details are still hidden; further details are received this way:
     5.6  *}
     5.7 -ML {* print_depth 99; @{term "a + b * 9"}; print_depth 5;
     5.8 +ML {* default_print_depth 99; @{term "a + b * 9"}; default_print_depth 5;
     5.9  *}
    5.10  text {* The internal representation is too comprehensive for several kinds of 
    5.11    inspection. Thus ISAC provides additional features, as we see below. First 

     6.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Mon Apr 20 10:33:55 2015 +0200
     6.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Mon Apr 20 14:18:40 2015 +0200
     6.3 @@ -33,7 +33,7 @@
     6.4  
     6.5    Please, skip this introductory ML-section in the first go ...*}
     6.6  ML {*
     6.7 -print_depth 1;
     6.8 +default_print_depth 1;
     6.9  val (thy, ro, er, inst) = 
    6.10      (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
    6.11  *}
    6.12 @@ -102,9 +102,9 @@
    6.13  text {* Now we want to bring 4*a close to 2*a in order to get 6*a:
    6.14  *}
    6.15  ML {*
    6.16 -val SOME (t, _) = rewrite_ thy ro er true @{thm add_assoc} t0; term2str t;
    6.17 -val SOME (t, _) = rewrite_ thy ro er true @{thm add_left_commute} t; term2str t;
    6.18 -val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t;
    6.19 +val SOME (t, _) = rewrite_ thy ro er true @{thm add.assoc} t0; term2str t;
    6.20 +val SOME (t, _) = rewrite_ thy ro er true @{thm add.left_commute} t; term2str t;
    6.21 +val SOME (t, _) = rewrite_ thy ro er true @{thm add.commute} t; term2str t;
    6.22  val SOME (t, _) = rewrite_ thy ro er true @{thm real_num_collect} t; term2str t;
    6.23  *}
    6.24  text {* That is fine, we just need to add 2+4 !!!!! See the next section below.
    6.25 @@ -115,10 +115,10 @@
    6.26    as one rule is applicable (that is the way such rulesets work).
    6.27    Try to step through the ML-sections without skipping one of them ...
    6.28  *}
    6.29 -ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t*}
    6.30 -ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t*}
    6.31 -ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t*}
    6.32 -ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t*}
    6.33 +ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add.commute} t; term2str t*}
    6.34 +ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add.commute} t; term2str t*}
    6.35 +ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add.commute} t; term2str t*}
    6.36 +ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add.commute} t; term2str t*}
    6.37  text {* ... you can go forever, the ruleset is 'not terminating'.
    6.38    The theory of rewriting makes this kind of rulesets terminate by the use of
    6.39    'rewrite orders': 

     7.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy	Mon Apr 20 10:33:55 2015 +0200
     7.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy	Mon Apr 20 14:18:40 2015 +0200
     7.3 @@ -110,17 +110,17 @@
     7.4  section {* Solving the example problem *}
     7.5  text {* Now let us observe, how the method ["simplification","for_polynomials",
     7.6    "with_minus"] guides through simplification by rewriting. For that purpose
     7.7 -  we increase the 'print_depth' (with the disadvantage of extending the output)
     7.8 +  we increase the 'default_print_depth' (with the disadvantage of extending the output)
     7.9    and print out the results by use of 'f2str'.
    7.10    Please, note only 'nxt' close to the beginning of the output and the resulting
    7.11    term at the end:
    7.12  *}
    7.13 -ML {* print_depth 40; *}
    7.14 +ML {* default_print_depth 40; *}
    7.15  ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
    7.16  ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
    7.17  ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
    7.18  ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
    7.19 -ML {* print_depth 3; *}
    7.20 +ML {* default_print_depth 3; *}
    7.21  text{* And, please, note that the result of applying the 'nxt' ruleset is to be
    7.22    found in the output of the next step !
    7.23  *}

     8.1 --- a/test/Tools/isac/Frontend/use-cases.sml	Mon Apr 20 10:33:55 2015 +0200
     8.2 +++ b/test/Tools/isac/Frontend/use-cases.sml	Mon Apr 20 14:18:40 2015 +0200
     8.3 @@ -343,7 +343,7 @@
     8.4   autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
     8.5   autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
     8.6   (*------------------------------------*)
     8.7 -(* print_depth 13; get_calc 1;
     8.8 +(* default_print_depth 13; get_calc 1;
     8.9     *)
    8.10   autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
    8.11   (*calc-head of subproblem*)
    8.12 @@ -1277,7 +1277,7 @@
    8.13   if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else 
    8.14   error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
    8.15  (* for getting the list in whole length ...
    8.16 -print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);print_depth 3;
    8.17 +default_print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);default_print_depth 3;
    8.18     *)
    8.19   if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = 
    8.20      [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),

     9.1 --- a/test/Tools/isac/Interpret/calchead.sml	Mon Apr 20 10:33:55 2015 +0200
     9.2 +++ b/test/Tools/isac/Interpret/calchead.sml	Mon Apr 20 14:18:40 2015 +0200
     9.3 @@ -39,14 +39,14 @@
     9.4   val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
     9.5   val ((pt,_),_) = get_calc 1;
     9.6  
     9.7 -print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
     9.8 +default_print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);default_print_depth 3;
     9.9  if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) = 
    9.10      [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), 
    9.11       ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
    9.12        ([3, 2], Res)] then () else
    9.13  error "calchead.sml: diff.behav. get_interval after replace} other 2 a";
    9.14  
    9.15 -print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); print_depth 3;
    9.16 +default_print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); default_print_depth 3;
    9.17  if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) = 
    9.18      [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
    9.19  error "modspec.sml: diff.behav. get_interval after replace} other 2 b";

    10.1 --- a/test/Tools/isac/Interpret/ctree.sml	Mon Apr 20 10:33:55 2015 +0200
    10.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Mon Apr 20 14:18:40 2015 +0200
    10.3 @@ -209,7 +209,7 @@
    10.4  "-------------- cut_level (from ptree above)----------------------";
    10.5  show_pt pt;
    10.6  show_pt pt';
    10.7 -print_depth 99; cuts; print_depth 3;
    10.8 +default_print_depth 99; cuts; default_print_depth 3;
    10.9  
   10.10  (*if cuts = [([2], Res),
   10.11  	   ([3], Frm),
   10.12 @@ -375,8 +375,8 @@
   10.13  
   10.14  show_pt pt;
   10.15  show_pt pt';
   10.16 -print_depth 99;cuts;print_depth 3;
   10.17 -print_depth 99;map fst (get_interval ([],Frm) ([],Res) 9999 pt');print_depth 3;
   10.18 +default_print_depth 99;cuts;default_print_depth 3;
   10.19 +default_print_depth 99;map fst (get_interval ([],Frm) ([],Res) 9999 pt');default_print_depth 3;
   10.20  ####################################################################*)
   10.21  
   10.22  
   10.23 @@ -1037,9 +1037,9 @@
   10.24  "-------------- get_allpos' new ----------------------------------";
   10.25  "-------------- get_allpos' new ----------------------------------";
   10.26  "--- whole ctree";
   10.27 -print_depth 99;
   10.28 +default_print_depth 99;
   10.29  val cuts = get_allp [] ([], ([],Frm)) pt;
   10.30 -print_depth 3;
   10.31 +default_print_depth 3;
   10.32  if cuts = 
   10.33     [(*never returns the first pos'*)
   10.34      ([1], Frm), 
   10.35 @@ -1056,9 +1056,9 @@
   10.36      ([], Res)] then () else
   10.37  error "ctree.sml diff.behav. get_allp new []";
   10.38  
   10.39 -print_depth 99;
   10.40 +default_print_depth 99;
   10.41  val cuts2 = get_allps [] [1] (children pt);
   10.42 -print_depth 3;
   10.43 +default_print_depth 3;
   10.44  if cuts = cuts2 @ [([], Res)] then () else
   10.45  error "ctree.sml diff.behav. get_allps new []";
   10.46  
   10.47 @@ -1128,9 +1128,9 @@
   10.48  
   10.49  "---(2) on S(606)..S(608)--------";
   10.50  val (pt', cuts) = cut_tree pt ([1],Res);
   10.51 -print_depth 99;
   10.52 +default_print_depth 99;
   10.53  cuts;
   10.54 -print_depth 3;
   10.55 +default_print_depth 3;
   10.56  if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
   10.57        ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
   10.58        ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
   10.59 @@ -1141,9 +1141,9 @@
   10.60  
   10.61  "---(3) on S(606)..S(608)--------";
   10.62  val (pt', cuts) = cut_tree pt ([2],Res);
   10.63 -print_depth 99;
   10.64 +default_print_depth 99;
   10.65  cuts;
   10.66 -print_depth 3;
   10.67 +default_print_depth 3;
   10.68  if cuts = [(*preceding step on WS was ([1]),Res*)
   10.69  	   ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
   10.70  	   ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), 
   10.71 @@ -1160,9 +1160,9 @@
   10.72  
   10.73  "---(4) on S(606)..S(608)--------";
   10.74  val (pt', cuts) = cut_tree pt ([3],Pbl);
   10.75 -print_depth 99;
   10.76 +default_print_depth 99;
   10.77  cuts;
   10.78 -print_depth 3;
   10.79 +default_print_depth 3;
   10.80  if cuts = [([3], Pbl),
   10.81  	   ([3, 1], Frm), ([3, 1], Res), 
   10.82  	   ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
   10.83 @@ -1174,9 +1174,9 @@
   10.84  
   10.85  "---(5a) on S(606)..S(608) cut_tree --------";
   10.86  val (pt', cuts) = cut_tree pt ([3,2,1],Res);
   10.87 -print_depth 99;
   10.88 +default_print_depth 99;
   10.89  cuts;
   10.90 -print_depth 1;
   10.91 +default_print_depth 1;
   10.92  if cuts = [([3, 2, 2], Res), ([3, 2], Res),
   10.93  (*WN060727 added after replacing cutlevup by test_trans:*)
   10.94  ([3], Res), ([4], Res),([],Res)] then () 
   10.95 @@ -1195,9 +1195,9 @@
   10.96  val (pt', cuts) = cappend_atomic pt [1] e_istate (str2term "Inform[1]")
   10.97      (Tac "test") (str2term "Inres[1]",[]) Complete;
   10.98  
   10.99 -print_depth 99;
  10.100 +default_print_depth 99;
  10.101  cuts;
  10.102 -print_depth 3;
  10.103 +default_print_depth 3;
  10.104  if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
  10.105        ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
  10.106        ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
  10.107 @@ -1206,9 +1206,9 @@
  10.108  else error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
  10.109  
  10.110  val afterins = get_allp [] ([], ([],Frm)) pt';
  10.111 -print_depth 99;
  10.112 +default_print_depth 99;
  10.113  afterins;
  10.114 -print_depth 3;
  10.115 +default_print_depth 3;
  10.116  if afterins = [([1], Frm), ([1], Res)
  10.117  (*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)] then()
  10.118  else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
  10.119 @@ -1217,9 +1217,9 @@
  10.120  show_pt pt;
  10.121  val (pt', cuts) = cappend_atomic pt [2] e_istate (str2term "Inform[2]")
  10.122      (Tac "test") (str2term "Inres[2]",[]) Complete;
  10.123 -print_depth 99;
  10.124 +default_print_depth 99;
  10.125  cuts;
  10.126 -print_depth 3;
  10.127 +default_print_depth 3;
  10.128  
  10.129  if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
  10.130        ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl), 
  10.131 @@ -1230,9 +1230,9 @@
  10.132  
  10.133  
  10.134  val afterins = get_allp [] ([], ([],Frm)) pt';
  10.135 -print_depth 99;
  10.136 +default_print_depth 99;
  10.137  afterins;
  10.138 -print_depth 3;
  10.139 +default_print_depth 3;
  10.140  
  10.141  if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)
  10.142  (*,  WN060727 removed after replacing cutlevup by test_trans:([], Res)*)] 
  10.143 @@ -1255,9 +1255,9 @@
  10.144  "---(4) on S(606)..S(608)--------";
  10.145  val (pt', cuts) = cappend_problem pt [3] e_istate ([],e_spec)
  10.146  				  ([],e_spec, str2term "Inhead[3]");
  10.147 -print_depth 99;
  10.148 +default_print_depth 99;
  10.149  cuts;
  10.150 -print_depth 3;
  10.151 +default_print_depth 3;
  10.152  if cuts = [([3], Pbl),
  10.153  	   ([3, 1], Frm), ([3, 1], Res), 
  10.154  	   ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
  10.155 @@ -1266,9 +1266,9 @@
  10.156  (*WN060727 added after replacing cutlevup by test_trans*)([], Res)] then ()else
  10.157  error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
  10.158  val afterins = get_allp [] ([], ([],Frm)) pt';
  10.159 -print_depth 99;
  10.160 +default_print_depth 99;
  10.161  afterins;
  10.162 -print_depth 3;
  10.163 +default_print_depth 3;
  10.164  if afterins = 
  10.165     [([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
  10.166      ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res),
  10.167 @@ -1281,18 +1281,18 @@
  10.168  "---(6-1) on S(606)..S(608)--------";
  10.169  val (pt', cuts) = cappend_atomic pt [3,1] e_istate (str2term "Inform[3,1]")
  10.170      (Tac "test") (str2term "Inres[3,1]",[]) Complete;
  10.171 -print_depth 99;
  10.172 +default_print_depth 99;
  10.173  cuts;
  10.174 -print_depth 3;
  10.175 +default_print_depth 3;
  10.176  if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), 
  10.177  	   ([3, 2], Res),
  10.178  (*WN060727 added*)([3], Res), ([4], Res), ([], Res)] then () else
  10.179  error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
  10.180  
  10.181  val afterins = get_allp [] ([], ([],Frm)) pt';
  10.182 -print_depth 99;
  10.183 +default_print_depth 99;
  10.184  afterins;
  10.185 -print_depth 3;
  10.186 +default_print_depth 3;
  10.187  (*WN060727 replaced after overwriting cutlevup by test_trans
  10.188  if afterins = [([1], Frm), ([1], Res), 
  10.189  	       ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
  10.190 @@ -1319,17 +1319,17 @@
  10.191  "---(6) on S(606)..S(608)--------";
  10.192  val (pt', cuts) = cappend_atomic pt [3,2] e_istate (str2term "Inform[3,2]")
  10.193      (Tac "test") (str2term "Inres[3,2]",[]) Complete;
  10.194 -print_depth 99;
  10.195 +default_print_depth 99;
  10.196  cuts;
  10.197 -print_depth 3;
  10.198 +default_print_depth 3;
  10.199  if cuts = [(*just after is: cutlevup=false in [3]*)
  10.200  (*WN060727 after test_trans instead cutlevup added:*)
  10.201  	   ([3], Res), ([4], Res), ([], Res)] then () else
  10.202  error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
  10.203  val afterins = get_allp [] ([], ([],Frm)) pt';
  10.204 -print_depth 99;
  10.205 +default_print_depth 99;
  10.206  afterins;
  10.207 -print_depth 3;
  10.208 +default_print_depth 3;
  10.209  (*WN060727 replaced after overwriting cutlevup by test_trans
  10.210  if afterins = [([1], Frm), ([1], Res), 
  10.211  	       ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
  10.212 @@ -1357,17 +1357,17 @@
  10.213  (**)
  10.214  val (pt', cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "Inform[3,2,1]")
  10.215      (Tac "test") (str2term "Inres[3,2,1]",[]) Complete;
  10.216 -print_depth 99;
  10.217 +default_print_depth 99;
  10.218  cuts;
  10.219 -print_depth 1;
  10.220 +default_print_depth 1;
  10.221  if cuts = [([3, 2, 2], Res), ([3, 2], Res),
  10.222  (*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)] 
  10.223  then () else
  10.224  error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
  10.225  val afterins = get_allp [] ([], ([],Frm)) pt';
  10.226 -print_depth 99;
  10.227 +default_print_depth 99;
  10.228  afterins;
  10.229 -print_depth 3;
  10.230 +default_print_depth 3;
  10.231  if afterins = [([1], Frm), ([1], Res), 
  10.232  	       ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
  10.233  	       ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), 

    11.1 --- a/test/Tools/isac/Interpret/inform.sml	Mon Apr 20 10:33:55 2015 +0200
    11.2 +++ b/test/Tools/isac/Interpret/inform.sml	Mon Apr 20 14:18:40 2015 +0200
    11.3 @@ -639,7 +639,7 @@
    11.4  val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
    11.5  val NONE = env;
    11.6  val (SOME istate, NONE) = loc;
    11.7 -print_depth 5;
    11.8 +default_print_depth 5;
    11.9  writeln"-----------------------------------------------------------";
   11.10  spec;
   11.11  writeln (itms2str_ ctxt probl);
   11.12 @@ -657,11 +657,11 @@
   11.13  val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
   11.14  val NONE = env;
   11.15  val (SOME istate, NONE) = loc;
   11.16 -print_depth 5; writeln (istate2str (fst istate));  print_depth 3;
   11.17 +default_print_depth 5; writeln (istate2str (fst istate));  default_print_depth 3;
   11.18  (*ScrState ([],
   11.19   [], NONE,
   11.20   ??.empty, Sundef, false)*)
   11.21 -print_depth 5; spec; print_depth 3;
   11.22 +default_print_depth 5; spec; default_print_depth 3;
   11.23  (*("Isac",
   11.24        ["derivative_of", "function"],
   11.25        ["diff", "differentiate_on_R"]) : spec*)
   11.26 @@ -700,11 +700,11 @@
   11.27  val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
   11.28  val NONE = env;
   11.29  val (SOME istate, NONE) = loc;
   11.30 -print_depth 5; writeln (istate2str (fst istate));  print_depth 3;
   11.31 +default_print_depth 5; writeln (istate2str (fst istate));  default_print_depth 3;
   11.32  (*ScrState ([],
   11.33   [], NONE,
   11.34   ??.empty, Sundef, false)*)
   11.35 -print_depth 5; spec; print_depth 3;
   11.36 +default_print_depth 5; spec; default_print_depth 3;
   11.37  (*("Isac",
   11.38        ["derivative_of", "function"],
   11.39        ["diff", "differentiate_on_R"]) : spec*)

    12.1 --- a/test/Tools/isac/Interpret/rewtools.sml	Mon Apr 20 10:33:55 2015 +0200
    12.2 +++ b/test/Tools/isac/Interpret/rewtools.sml	Mon Apr 20 14:18:40 2015 +0200
    12.3 @@ -253,7 +253,7 @@
    12.4  "----------- fun guh2theID ------------------------------";
    12.5  "----------- fun guh2theID ------------------------------";
    12.6  val guh = "thy_scri_ListG-thm-zip_Nil";
    12.7 -print_depth 3; (*999*)
    12.8 +default_print_depth 3; (*999*)
    12.9  take_fromto 1 4 (Symbol.explode guh);
   12.10  take_fromto 5 9 (Symbol.explode guh);
   12.11  val rest = takerest (9,(Symbol.explode guh)); 

    13.1 --- a/test/Tools/isac/Interpret/solve.sml	Mon Apr 20 10:33:55 2015 +0200
    13.2 +++ b/test/Tools/isac/Interpret/solve.sml	Mon Apr 20 14:18:40 2015 +0200
    13.3 @@ -9,7 +9,7 @@
    13.4  uses from Poly.ML: Rls make_polynomial, Rls expand_binom 
    13.5  *)
    13.6  
    13.7 -print_depth 5;
    13.8 +default_print_depth 5;
    13.9  trace_rewrite := false;
   13.10  trace_script := false;
   13.11  "-----------------------------------------------------------------";

    14.1 --- a/test/Tools/isac/Knowledge/atools.sml	Mon Apr 20 10:33:55 2015 +0200
    14.2 +++ b/test/Tools/isac/Knowledge/atools.sml	Mon Apr 20 14:18:40 2015 +0200
    14.3 @@ -7,7 +7,7 @@
    14.4  use"atools.sml";
    14.5  *)
    14.6  
    14.7 -print_depth 5;
    14.8 +default_print_depth 5;
    14.9  "--------------------------------------------------------";
   14.10  "table of contents --------------------------------------";
   14.11  "--------------------------------------------------------";

    15.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml	Mon Apr 20 10:33:55 2015 +0200
    15.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml	Mon Apr 20 14:18:40 2015 +0200
    15.3 @@ -424,7 +424,7 @@
    15.4  trace_rewrite := false;
    15.5  val matches = refine fmz ["2x2", "LINEAR","system"];
    15.6  trace_rewrite:=false;
    15.7 -print_depth 11; matches; print_depth 3;
    15.8 +default_print_depth 11; matches; default_print_depth 3;
    15.9  (*brought: 'False "length_ es_ = 2"'*)
   15.10  
   15.11  (*-----fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) =

    16.1 --- a/test/Tools/isac/Knowledge/gcd_poly_winkler.sml	Mon Apr 20 10:33:55 2015 +0200
    16.2 +++ b/test/Tools/isac/Knowledge/gcd_poly_winkler.sml	Mon Apr 20 14:18:40 2015 +0200
    16.3 @@ -86,7 +86,7 @@
    16.4    doe not conform with the Isabelle coding standards)
    16.5  *}*)
    16.6  
    16.7 - print_depth 3; (*20*)
    16.8 + default_print_depth 3; (*20*)
    16.9   type unipoly = int list;
   16.10  
   16.11  "----------- auxiliary functions univariate -------------";

    17.1 --- a/test/Tools/isac/Knowledge/poly.sml	Mon Apr 20 10:33:55 2015 +0200
    17.2 +++ b/test/Tools/isac/Knowledge/poly.sml	Mon Apr 20 14:18:40 2015 +0200
    17.3 @@ -373,9 +373,9 @@
    17.4  (*...if there is an error, then ...*)
    17.5  
    17.6  "-----1 ---";
    17.7 -print_depth 7;
    17.8 +default_print_depth 7;
    17.9  val pbt = get_pbt ["polynomial","simplification"];
   17.10 -print_depth 3;
   17.11 +default_print_depth 3;
   17.12  (*if there is ...
   17.13  > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
   17.14  ... then trace_rewrite:*)
   17.15 @@ -387,9 +387,9 @@
   17.16  (*... if there is no rewrite, then there is something wrong with prls*)
   17.17                                
   17.18  "-----3 ---";
   17.19 -print_depth 7;
   17.20 +default_print_depth 7;
   17.21  val prls = (#prls o get_pbt) ["polynomial","simplification"];
   17.22 -print_depth 3;
   17.23 +default_print_depth 3;
   17.24  val t = str2term "((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)) is_polyexp";
   17.25  val SOME (t',_) = rewrite_set_ thy false prls t;
   17.26  if t' = @{term True} then () 

    18.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Mon Apr 20 10:33:55 2015 +0200
    18.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Mon Apr 20 14:18:40 2015 +0200
    18.3 @@ -550,9 +550,9 @@
    18.4  "----------- refine Vereinfache ----------------------------------";
    18.5  "----------- refine Vereinfache ----------------------------------";
    18.6  val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*(q::real)))", "normalform (N::real)"];
    18.7 -print_depth 11;
    18.8 +default_print_depth 11;
    18.9  val matches = refine fmz ["vereinfachen"];
   18.10 -print_depth 3;
   18.11 +default_print_depth 3;
   18.12  
   18.13  "----- go into details, if it seems not to work -----";
   18.14  "--- does the predicate evaluate correctly ?";

    19.1 --- a/test/Tools/isac/Knowledge/rational.sml	Mon Apr 20 10:33:55 2015 +0200
    19.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Mon Apr 20 14:18:40 2015 +0200
    19.3 @@ -350,9 +350,9 @@
    19.4          val vs = t |> vars |> map free2str |> sort string_ord
    19.5          val baseT = type_of numerator
    19.6          val expT = HOLogic.realT;
    19.7 -print_depth 3; (*999*)
    19.8 +default_print_depth 3; (*999*)
    19.9  val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator);
   19.10 -print_depth 3; (*999*)
   19.11 +default_print_depth 3; (*999*)
   19.12  (* does not terminate instead of returning ?:
   19.13          val ((a', b'), c) = gcd_poly a b
   19.14  val a = [(~12, [0, 0]), (3, [2, 0]), (4, [0, 1]), (~1, [2, 1])]: poly
   19.15 @@ -413,10 +413,10 @@
   19.16  term2str n1; term2str d1; term2str n2; term2str d2;
   19.17        val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *)
   19.18          |> filter is_some |> map the |> sort string_ord;
   19.19 -print_depth 3; (*999*)
   19.20 +default_print_depth 3; (*999*)
   19.21  val (SOME _, SOME a, SOME _, SOME b) =
   19.22    (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2);
   19.23 -print_depth 3; (*999*)
   19.24 +default_print_depth 3; (*999*)
   19.25  (*
   19.26  val a = [(1, [1, 0, 0]), (~1, [0, 1, 1])]: poly
   19.27  val b = [(1, [1, 0, 0]), (1, [0, 1, 1])]: poly
   19.28 @@ -796,7 +796,7 @@
   19.29  (* WN.10.10.02: dieser Fall terminiert nicht 
   19.30             (make_polynomial enth"alt zu viele rules)
   19.31  WN060823 'init_state' requires rewriting on specified location in the term
   19.32 -print_depth 99; Rfuns; print_depth 3;
   19.33 +default_print_depth 99; Rfuns; default_print_depth 3;
   19.34  WN060831 cycling "sym_order_mult_rls_" "sym_mult_assoc"
   19.35           as was with make_polynomial before ?!?*)
   19.36  
   19.37 @@ -1581,22 +1581,22 @@
   19.38  val {rules, rew_ord= (_, ro), ...} = rep_rls (assoc_rls "rev_rew_p");
   19.39  val der = make_deriv thy Atools_erls rules ro NONE tt;
   19.40  if length der = 12 then () else error "WN1130912 rls chancel_p 4";
   19.41 -print_depth 99; writeln (deriv2str der); print_depth 3;
   19.42 +default_print_depth 99; writeln (deriv2str der); default_print_depth 3;
   19.43  
   19.44 -print_depth 99; map (term2str o #1) der; print_depth 3;
   19.45 +default_print_depth 99; map (term2str o #1) der; default_print_depth 3;
   19.46  "...,(-1 * b ^^^ 2 + a ^^^ 2) / (-2 * (a * b) + a ^^^ 2 + (-1 * b) ^^^ 2) ]";
   19.47 -print_depth 99; map (rule2str o #2) der; print_depth 3;
   19.48 -print_depth 99; map (term2str o #1 o #3) der; print_depth 3;
   19.49 +default_print_depth 99; map (rule2str o #2) der; default_print_depth 3;
   19.50 +default_print_depth 99; map (term2str o #1 o #3) der; default_print_depth 3;
   19.51  
   19.52  val der = make_deriv thy Atools_erls rules ro NONE 
   19.53  	(str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");
   19.54 -print_depth 99; writeln (deriv2str der); print_depth 3;
   19.55 +default_print_depth 99; writeln (deriv2str der); default_print_depth 3;
   19.56  
   19.57  val {rules, rew_ord=(_,ro),...} = rep_rls (assoc_rls "rev_rew_p");
   19.58  val der = make_deriv thy Atools_erls rules ro NONE 
   19.59  	(str2term "(1 * a + -1 * b) * (1 * a + -1 * b)");
   19.60 -print_depth 99; writeln (deriv2str der); print_depth 3;
   19.61 -print_depth 99; map (term2str o #1) der; print_depth 3;
   19.62 +default_print_depth 99; writeln (deriv2str der); default_print_depth 3;
   19.63 +default_print_depth 99; map (term2str o #1) der; default_print_depth 3;
   19.64  (*WN060829 ...postponed*)
   19.65  
   19.66  

    20.1 --- a/test/Tools/isac/Knowledge/system.sml	Mon Apr 20 10:33:55 2015 +0200
    20.2 +++ b/test/Tools/isac/Knowledge/system.sml	Mon Apr 20 14:18:40 2015 +0200
    20.3 @@ -96,7 +96,7 @@
    20.4  case nxt of ("End_Proof'", End_Proof') => ()
    20.5  	  | _ => error  "system.sml diff.behav.in me --99";
    20.6  
    20.7 -print_depth 11;nxt;print_depth 3;
    20.8 +default_print_depth 11;nxt;default_print_depth 3;
    20.9  ---*)
   20.10  (*
   20.11  use"../smltest/IsacKnowledge/system.sml";

    21.1 --- a/test/Tools/isac/OLDTESTS/modspec.sml	Mon Apr 20 10:33:55 2015 +0200
    21.2 +++ b/test/Tools/isac/OLDTESTS/modspec.sml	Mon Apr 20 14:18:40 2015 +0200
    21.3 @@ -24,14 +24,14 @@
    21.4   val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
    21.5   val ((pt,_),_) = get_calc 1;
    21.6  
    21.7 -print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
    21.8 +default_print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);default_print_depth 3;
    21.9  if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) = 
   21.10      [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), 
   21.11       ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
   21.12        ([3, 2], Res)] then () else
   21.13  error "modspec.sml: diff.behav. get_interval after replace} other 2 a";
   21.14  
   21.15 -print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); print_depth 3;
   21.16 +default_print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); default_print_depth 3;
   21.17  if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) = 
   21.18      [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
   21.19  error "modspec.sml: diff.behav. get_interval after replace} other 2 b";

    22.1 --- a/test/Tools/isac/ProgLang/termC.sml	Mon Apr 20 10:33:55 2015 +0200
    22.2 +++ b/test/Tools/isac/ProgLang/termC.sml	Mon Apr 20 14:18:40 2015 +0200
    22.3 @@ -183,7 +183,7 @@
    22.4    "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n==>" ^
    22.5    " (?a + ?b = ?c) = (?b = ?c + -1 * ?a)"
    22.6  then () else error "termC.sml separate_bdvs_add";
    22.7 -print_depth 5; 
    22.8 +default_print_depth 5; 
    22.9  
   22.10  val subst = 
   22.11    [(str2term "bdv_1", str2term "c"),
   22.12 @@ -222,7 +222,7 @@
   22.13   val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = (c::real)";
   22.14   (*        !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*)
   22.15   val insts = Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty);
   22.16 -print_depth 3; (*999*) insts; 
   22.17 +default_print_depth 3; (*999*) insts; 
   22.18   (*val insts =
   22.19     ({}, 
   22.20      {(("a", 0), ("Real.real", Free ("3", "Real.real"))), 

    23.1 --- a/test/Tools/isac/calcelems.sml	Mon Apr 20 10:33:55 2015 +0200
    23.2 +++ b/test/Tools/isac/calcelems.sml	Mon Apr 20 14:18:40 2015 +0200
    23.3 @@ -74,7 +74,7 @@
    23.4  pretty types:
    23.5   PolyML.addPrettyPrinter
    23.6     (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
    23.7 - print_depth 3;
    23.8 + default_print_depth 3;
    23.9  *)
   23.10  "===== extend parse to string with markup===";
   23.11  (*

    24.1 --- a/test/Tools/isac/xmlsrc/datatypes.sml	Mon Apr 20 10:33:55 2015 +0200
    24.2 +++ b/test/Tools/isac/xmlsrc/datatypes.sml	Mon Apr 20 14:18:40 2015 +0200
    24.3 @@ -32,7 +32,7 @@
    24.4  "~~~~~ fun get_the, args:"; val (theID:theID) = (["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]);
    24.5  (*get_py  (Thy_Info.get_theory "Pure") theID theID (get_thes ()); 
    24.6    (* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
    24.7 -print_depth 3; (*999*)
    24.8 +default_print_depth 3; (*999*)
    24.9  (get_thes ());
   24.10  
   24.11  (*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((Thy_Info.get_theory "Pure"), theID, theID, (get_thes ()));*)