test/Tools/isac/Knowledge/diffapp.sml
branchdecompose-isar
changeset 42195 ac2c5fb8fedd
parent 42166 911c49949ba9
child 42203 8e216c5001bd
     1.1 --- a/test/Tools/isac/Knowledge/diffapp.sml	Fri Jul 22 14:01:52 2011 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml	Mon Jul 25 08:31:53 2011 +0200
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  (* tests for IsacKnowledge/DiffApp
     1.6     author Walther Neuper 000301
     1.7     (c) due to copyright terms
     1.8 @@ -20,7 +21,6 @@
     1.9  "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
    1.10  
    1.11  
    1.12 -(*=== inhibit exn 110722=============================================================
    1.13  
    1.14  
    1.15  
    1.16 @@ -29,8 +29,10 @@
    1.17  " #################################################### ";
    1.18  " -------------- [maximum_of,function] --------------- ";
    1.19  val pbt = 
    1.20 -    ["fixedValues f_ix","maximum m_","valuesFor v_s","relations r_s"];
    1.21 +    ["fixedValues f_ix","maximum m_m","valuesFor v_s","relations r_s"];
    1.22 +(*=== inhibit exn 110722=============================================================
    1.23  map (the o (parseold thy)) pbt;
    1.24 +=== inhibit exn 110722=============================================================*)
    1.25  val fmz =
    1.26      ["fixedValues [r=Arbfix]","maximum A",
    1.27       "valuesFor [a,b]",
    1.28 @@ -43,11 +45,14 @@
    1.29       "interval {x::real. 0 <= x & x <= 2*r}",
    1.30       "interval {x::real. 0 <= x & x <= pi}",
    1.31       "errorBound (eps=(0::real))"];
    1.32 +(*=== inhibit exn 110722=============================================================
    1.33  map (the o (parseold thy)) fmz;
    1.34  " -------------- [make,function] -------------- ";
    1.35 +=== inhibit exn 110722=============================================================*)
    1.36  val pbt = 
    1.37      ["functionOf f_f","boundVariable v_v","equalities eqs",
    1.38 -     "functionTerm f_0_"];
    1.39 +     "functionTerm f_0_0"];
    1.40 +(*=== inhibit exn 110722=============================================================
    1.41  map (the o (parseold thy)) pbt;
    1.42  val fmz12 =
    1.43      ["functionOf A","boundVariable a","boundVariable b",
    1.44 @@ -61,7 +66,7 @@
    1.45  map (the o (parseold thy)) fmz3;
    1.46  " --------- [univar,equation] --------- ";
    1.47  val pbt = 
    1.48 -    ["equality e_e","solveFor v_v","solutions v_i_"];
    1.49 +    ["equality e_e","solveFor v_v","solutions v_i_i"];
    1.50  map (the o (parseold thy)) pbt;
    1.51  val fmz =
    1.52      ["equality ((a/2)^^^2 + (b/2)^^^2 = r^^^2)",
    1.53 @@ -69,8 +74,8 @@
    1.54  map (the o (parseold thy)) fmz;
    1.55  " ---- [on_interval,maximum_of,function] ---- ";
    1.56  val pbt = 
    1.57 -    ["functionTerm t_","boundVariable v_v","interval itv_",
    1.58 -     "errorBound err_","maxArgument v_0"];
    1.59 +    ["functionTerm t_t","boundVariable v_v","interval itv_v",
    1.60 +     "errorBound err_r","maxArgument v_0"];
    1.61  map (the o (parseold thy)) pbt;
    1.62  val fmz12 =
    1.63      [(*28.11.00: "functionTerm (A_0 = a*sqrt(#4*r^^^#2 - a^^^#2))",*)
    1.64 @@ -100,8 +105,8 @@
    1.65  map (the o (parseold thy)) fmz;
    1.66  " --------- [find_values,tool] --------- ";
    1.67  val pbt = 
    1.68 -    ["maxArgument ma_","functionTerm f_f","boundVariable v_v",
    1.69 -     "valuesFor vls_","additionalRels r_s"];
    1.70 +    ["maxArgument ma_a","functionTerm f_f","boundVariable v_v",
    1.71 +     "valuesFor vls_s","additionalRels r_s"];
    1.72  map (the o (parseold thy)) pbt;
    1.73  val fmz1 =
    1.74      ["maxArgument (a_0=(srqt 2)*r)",
    1.75 @@ -762,3 +767,4 @@
    1.76  
    1.77  
    1.78  ===== inhibit exn 110722===========================================================*)
    1.79 +