test/Tools/isac/Interpret/inform.sml
branchisac-update-Isa09-2
changeset 38050 4c52ad406c20
parent 38031 460c24a6a6ba
child 38058 ad0485155c0e
     1.1 --- a/test/Tools/isac/Interpret/inform.sml	Wed Oct 06 14:52:12 2010 +0200
     1.2 +++ b/test/Tools/isac/Interpret/inform.sml	Wed Oct 06 15:12:41 2010 +0200
     1.3 @@ -101,13 +101,13 @@
     1.4  
     1.5     *)
     1.6  "----------------------------------------------------------";
     1.7 - val fod = make_deriv Isac.thy Atools_erls 
     1.8 + val fod = make_deriv (theory "Isac") Atools_erls 
     1.9  		       ((#rules o rep_rls) Test_simplify)
    1.10  		       (sqrt_right false (theory "Pure")) NONE 
    1.11  		       (str2term "x + 1 + -1 * 2 = 0");
    1.12   (writeln o trtas2str) fod;
    1.13  
    1.14 - val ifod = make_deriv Isac.thy Atools_erls 
    1.15 + val ifod = make_deriv (theory "Isac") Atools_erls 
    1.16  		       ((#rules o rep_rls) Test_simplify)
    1.17  		       (sqrt_right false (theory "Pure")) NONE 
    1.18  		       (str2term "-2 * 1 + (1 + x) = 0");
    1.19 @@ -544,7 +544,7 @@
    1.20   [], NONE,
    1.21   ??.empty, Sundef, false)*)
    1.22  print_depth 5; spec; print_depth 3;
    1.23 -(*("Isac.thy",
    1.24 +(*("Isac",
    1.25        ["derivative_of", "function"],
    1.26        ["diff", "differentiate_on_R"]) : spec*)
    1.27  writeln (itms2str_ ctxt probl);
    1.28 @@ -574,7 +574,7 @@
    1.29  (*the following input is copied from BridgeLog Java <==> SML,
    1.30    omitting unnecessary inputs*)
    1.31  (*1>*)states:=[];
    1.32 -(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_"],("Isac.thy",["derivative_of","function"],["diff","differentiate_on_R"]))];
    1.33 +(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_"],("Isac",["derivative_of","function"],["diff","differentiate_on_R"]))];
    1.34  (*3>*)Iterator 1; moveActiveRoot 1;
    1.35  
    1.36  (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
    1.37 @@ -589,7 +589,7 @@
    1.38   [], NONE,
    1.39   ??.empty, Sundef, false)*)
    1.40  print_depth 5; spec; print_depth 3;
    1.41 -(*("Isac.thy",
    1.42 +(*("Isac",
    1.43        ["derivative_of", "function"],
    1.44        ["diff", "differentiate_on_R"]) : spec*)
    1.45  writeln (itms2str_ ctxt probl);