wneuper/isac: src/sml/systest/testdaten.sml@90390fecbe74

     1 (* testdaten f"ur isac demo0

     2    WN 31.10.00, .., 18.1.01

     3    use"tests/testdaten.sml";

     4    use"testdaten.sml";

     6    proofs:= []; dials:=([],[],[]);

     7   *)

     8 " _________________ exampel [x=4]: Rules 4.2.01a________________ ";

     9 " _________________ exampel [x=4]: Rules 4.2.01b________________ ";

    10 " _________________ exampel [x=4]: tutor active ________________ ";

    11 " _________________ exampel [x=4] ________________ ";

    12 " _________________ exampel [x =(-12)/5] ________________ ";

    13 " _________________ exampel [x =(-12)/5] Auto ________________ ";

    14 " ----------------- d_d x (x ^^^ 2 + 3 * x + 4) ----------------- ";

    15 " ----------------- d_d x (x ^^^ 2 + x + 1 / x ^^^ 2) ----------------- ";

    16 " ----------------- Schalk III S.62 Nr. 51a) --------- ";

    17 " ----------------- Schalk III S.144 Nr. 408b) --------- ";

    18 " ----------------- Schalk III S.137 Nr. 359g) --------- ";

    24 " _________________ exampel [x=4]: Rules 4.2.01a________________ ";

    25 " _________________ exampel [x=4]: Rules 4.2.01a________________ ";

    26 val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User;

    27 val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof;

    28 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

    29 	   "solveFor x","errorBound (eps=0)",

    30 	   "solutions L"];

    31 val (dI',pI',mI') =

    32   ("Test.thy",["squareroot","univariate","equation","test"],

    33    ("Test.thy","sqrt-equ-test"));

    34 "--- 0 ---";

    35 StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

    36 "--- 1 ---";

    37 StdinSML uI pI ~1 ~1 (Command Accept);

    38 (* square_equation_left

    39 "#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2"*)

    40 "--- 2 ---";

    41 StdinSML uI pI ~2 ~2 (Command Rules);

    42 "--- 3 ---";

    43 StdinSML uI pI ~2 ~2 (RuleFK (Rewrite_Set "Test_simplify"));

    44 "--- 4 ---";

    45 val (_,_,_,_,_,[Error_ _ (*"Error_ Test_simplify not applicable to ..*),

    46     Request "apply a rule !"],_) =

    47 StdinSML uI pI ~3 ~3 (RuleFK (Rewrite_Set "Test_simplify"));

    50 " _________________ exampel [x=4]: Rules 4.2.01b________________ ";

    51 " _________________ exampel [x=4]: Rules 4.2.01b________________ ";

    52 val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User;

    53 val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof;

    54 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

    55 	   "solveFor x","errorBound (eps=0)",

    56 	   "solutions L"];

    57 val (dI',pI',mI') =

    58   ("Test.thy",["squareroot","univariate","equation","test"],

    59    ("Test.thy","sqrt-equ-test"));

    60 "--- 0 ---";

    61 StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

    62 "--- 1 ---";

    63 StdinSML uI pI ~1 ~1 (Command Accept);

    64 (* square_equation_left

    65 "#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2"*)

    66 "--- 2 ---";

    67 StdinSML uI pI ~2 ~2 (Command Rules);

    68 "--- 3 ---";

    69 val (_,_,_,_,_,

    70    [Error_ _ (*"Error_ 'square_equation_left' not applicable to: #9 *),

    71     Select _, Request "select a rule !"],_) =

    72 StdinSML uI pI ~2 ~2 (RuleFK (Rewrite ("square_equation_left","")));

    75 " _________________ exampel [x=4]: tutor active ________________ ";

    76 " _________________ exampel [x=4]: tutor active ________________ ";

    77 val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User;

    78 val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof;

    79 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

    80 	   "solveFor x","errorBound (eps=0)",

    81 	   "solutions L"];

    82 val (dI',pI',mI') =

    83   ("Test.thy",["squareroot","univariate","equation","test"],

    84    ("Test.thy","sqrt-equ-test"));

    85 "--- s1 ---";

    86 StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

    87 "--- 1 ---";

    88 StdinSML uI pI ~1 ~1 (Command Accept);

    89 (* square_equation_left

    90 "#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2"*)

    91 "--- 2 ---";

    92 StdinSML uI pI ~2 ~2 (Command Accept);

    93 (* Test_simplify

    94 "#9 + #4 * x = #5 + (#2 * x + #2 * sqrt (x ^^^ #2 + #5 * x))"*)

    95 "--- 3 ---";

    96 StdinSML uI pI ~3 ~3 (Command Accept);

    97 (* rearrange_assoc

    98 "#9 + #4 * x = #5 + #2 * x + #2 * sqrt (x ^^^ #2 + #5 * x)"*)

    99 "--- 4 ---";

   100 StdinSML uI pI ~4 ~4 (Command Accept);

   101 (* isolate_root

   102 "sqrt (x ^^^ #2 + #5 * x) = (#5 + #2 * x + #-1 * (#9 + #4 * x)) // (#-1 *#2)"*)

   103 "--- 5 ---";

   104 StdinSML uI pI ~5 ~5 (Command Accept);

   105 (* Test_simplify

   106 "sqrt (x ^^^ #2 + #5 * x) = #2 + x"*)

   107 "--- 6 ---";

   108 StdinSML uI pI ~6 ~6 (Command Accept);

   109 (* square_equation_left

   110 "x ^^^ #2 + #5 * x = (#2 + x) ^^^ #2"*)

   111 "--- 7 ---";

   112 StdinSML uI pI ~7 ~7 (Command Accept);

   113 (* Test_simplify

   114 "x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)"*)

   115 "--- 8 ---";

   116 StdinSML uI pI ~8 ~8 (Command Accept);

   117 (* rearrange_assoc

   118 "x ^^^ #2 + #5 * x = #4 + x ^^^ #2 + #4 * x"*)

   119 "--- 9 ---";

   120 StdinSML uI pI ~9 ~9 (Command Accept);

   121 (* Test_simplify

   122 "x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)"*)

   123 "--- 10 ---";

   124 StdinSML uI pI ~10 ~10 (Command Accept);

   125 (* norm_equation

   126 "x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0"*)

   127 "--- 11 ---";

   128 StdinSML uI pI ~11 ~11 (Command Accept);

   129 (* Test_simplify

   130  "#-4 + x = #0"*)

   131 "--- 12 ---";

   132 StdinSML uI pI ~12 ~12 (Command Accept);

   133 (* isolate_bdv

   134 "x = #0 + #-1 * #-4" *)

   135 "--- 13 ---";

   136 StdinSML uI pI ~13 ~13 (Command Accept);

   137 (* Test_simplify

   138 "x = #4" *)

   139 "--- 14 ---";

   140 StdinSML uI pI ~14 ~14 (Command Accept);

   141 val (_,_,1,~14,[],[RuleKF (_,m),FormKF (_,_,_,_,f),Request "Accept ?"],_) = it;

   142 if m = Check_Postcond ["squareroot","univariate","equation","test"]

   143    andalso f = "[x = 4]" then ()

   144 else raise error "new behaviour in: exampel [x=4]: tutor active";

   145 "--- 15 ---";

   146 StdinSML uI pI ~15 ~15 (Command Accept);

   147 (* Request "start another example"*)

   149 (*---- after restruct. kb 18.9.02 ---- (same is in test-FE...)

   150 " _________________ exampel [x=4] ________________ ";

   151 " _________________ exampel [x=4] ________________ ";

   152 proofs:= []; dials:=([],[],[]);

   153 StdinSML 0 0 0 0 New_User;

   154 StdinSML 1 0 0 0 New_Proof;

   155 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

   156 	   "solveFor x","errorBound (eps=0)",

   157 	   "solutions L"];

   158 val (dI',pI',mI') =

   159   ("Test.thy",["squareroot","univariate","equation","test"],

   160    ("Test.thy","sqrt-equ-test"));

   161 "--- s1 ---";

   162 val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),req],_) =

   163 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

   165 StdinSML 1 1 ~1 ~1 (Command ActivePlus);

   166 StdinSML 1 1 ~1 ~1 (Command ActivePlus);

   167 StdinSML 1 1 ~1 ~1 (Command ActivePlus);

   168 StdinSML 1 1 ~1 ~1 (Command ActivePlus);(*acti=4..SelRule*)

   170 "--- !!! x1 --- strange choice"; (* hier nochmals spec !*)

   171 StdinSML 1 1 ~1  ~1 (RuleFK (Rewrite_Set "norm_equation"));

   172 "--- !!! x2 --- ME knows nxt_step";

   173 StdinSML 1 1 ~2  ~2 (RuleFK (Rewrite_Set "Test_simplify"));

   174 "--- !!! x3 --- helpless !!!";

   175 val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) =

   176 StdinSML 1 1 ~3  ~3 (RuleFK (Rewrite_Set "rearrange_assoc"));

   177 "--- !!! x4 ---";

   178 val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) =

   179 StdinSML 1 1 ~4  ~4 (RuleFK (Rewrite_Set "isolate_root"));

   180 "--- !!! x5 --- back at original equation !!!";

   181 val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) =

   182 StdinSML 1 1 ~5   ~5 (RuleFK (Rewrite_Set "Test_simplify"));

   183 if res="sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"

   184 then () else raise error "new behaviour in test-example";

   185 "--- !!! x6 --- not applicable";

   186 val (_,_,_,_,_,[Error_ err,_,requ],_) =

   187 StdinSML 1 1 ~6  ~6 (RuleFK (Rewrite_Set "Test_simplify"));

   188 (*val (_,_,_,_,_,[RuleKF r,requ],_) =*)

   189 val (_,_,_,_,_,ios,_) =

   190 StdinSML 1 1 ~6 ~6 (Command YourTurn);

   191 StdinSML 1 1 ~7 ~7 (Command Accept);

   192 StdinSML 1 1 ~8 ~8 (Command Accept);

   193 StdinSML 1 1 ~9 ~9 (Command Accept);

   194 StdinSML 1 1 ~10 ~10 (Command Accept);

   195 StdinSML 1 1 ~11 ~11 (Command Accept);

   196 StdinSML 1 1 ~12 ~12 (Command Accept);

   197 StdinSML 1 1 ~13 ~13 (Command Accept);

   198 StdinSML 1 1 ~14 ~14 (Command Accept);

   199 StdinSML 1 1 ~15 ~15 (Command Accept);

   200 StdinSML 1 1 ~16 ~16 (Command Accept);

   201 StdinSML 1 1 ~17 ~17 (Command Accept);

   202 StdinSML 1 1 ~18 ~18 (Command Accept);

   203 StdinSML 1 1 ~19 ~19 (Command Accept);

   204 val (_,1,1,_,[],[FormKF (_,_,_,_,f),Request "Accept ?"],_) = it;

   205 if f="[x = 4]" then () else raise error "new behaviour in test-example[x=4]";

   207 val (_,1,1,~20,[],[Request "start another example",End_Proof],_) =

   208 StdinSML 1 1 ~20 ~20 (Command Accept);

   209 -------------------------------------------------------------------*)

   213 " _________________ exampel [x =(-12)/5] ________________ ";

   214 " _________________ exampel [x =(-12)/5] ________________ ";

   215 proofs:= []; dials:=([],[],[]);

   216 StdinSML 0 0 0 0 New_User;

   217 StdinSML 1 0 0 0 New_Proof;

   218 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))",

   219 	   "solveFor x","errorBound (eps=0)",

   220 	   "solutions L"];

   221 val (dI',pI',mI') =

   222   ("Test.thy",["squareroot","univariate","equation","test"],

   223    ("Test.thy","sqrt-equ-test"));

   224 "--- s1 ---";

   225 val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),req],_) =

   226 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

   228 StdinSML 1 1 ~1 ~1 (Command SpeedMinus);

   229 StdinSML 1 1 ~1 ~1 (Command SpeedMinus);

   230 StdinSML 1 1 ~1 ~1 (Command Accept);(*->rule*)

   231 StdinSML 1 1 ~1 ~1 (Command Accept);(*->form*)

   232 val (_,_,_,_,_,dats,_) =

   233 StdinSML 1 1 ~2 ~2 (Command Accept);(*->rule*)

   234 StdinSML 1 1 ~2 ~2 (Command Accept);(*->form*)

   237 StdinSML 1 1 ~3 ~3 (Command ActivePlus);

   238 StdinSML 1 1 ~3 ~3 (Command ActivePlus);(*act=2: SelRule..PutRuleRes,Tt*)

   239 StdinSML 1 1 ~3 ~3 (RuleFK (Rewrite_Set "rearrange_assoc"));

   240 StdinSML 1 1 ~4 ~4 (Command Accept);

   241 StdinSML 1 1 ~4 ~4 (RuleFK (Rewrite_Set "isolate_root"));

   242 StdinSML 1 1 ~5 ~5 (Command Accept);

   243 StdinSML 1 1 ~5 ~5 (RuleFK (Rewrite_Set "Test_simplify"));

   244 StdinSML 1 1 ~6 ~6 (Command Accept);

   247 StdinSML 1 1 ~6 ~6 (Command SpeedPlus);

   248 StdinSML 1 1 ~6 ~6 (Command SpeedPlus);(*act=2: SelRule..SelRule*)

   249 StdinSML 1 1 ~6 ~6 (RuleFK (Rewrite ("square_equation_left","")));

   250 StdinSML 1 1 ~7 ~7 (RuleFK (Rewrite_Set "Test_simplify"));

   251 StdinSML 1 1 ~8 ~8 (RuleFK (Rewrite_Set "rearrange_assoc"));

   254 StdinSML 1 1 ~9 ~9 (Command YourTurn);

   255 StdinSML 1 1 ~10 ~10 (Command Accept);

   256 StdinSML 1 1 ~11 ~11 (Command Accept);

   257 StdinSML 1 1 ~12 ~12 (Command Accept);

   258 StdinSML 1 1 ~13 ~13 (Command Accept);

   259 StdinSML 1 1 ~14 ~14 (Command Accept);

   260 val (_,_,_,_,_,dats,_) =

   261 StdinSML 1 1 ~15 ~15 (Command Accept);

   262 if dats=[Request "start another example",End_Proof] then ()

   263 else raise error "new behaviour in test-example 1: [x =(-12)/5]";

   266 " _________________ exampel [x =(-12)/5] Auto ________________ ";

   267 " _________________ exampel [x =(-12)/5] Auto ________________ ";

   268 proofs:= []; dials:=([],[],[]);

   269 StdinSML 0 0 0 0 New_User;

   270 StdinSML 1 0 0 0 New_Proof;

   271 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))",

   272 	   "solveFor x","errorBound (eps=0)",

   273 	   "solutions L"];

   274 val (dI',pI',mI') =

   275   ("Test.thy",["squareroot","univariate","equation","test"],

   276    ("Test.thy","sqrt-equ-test"));

   277 val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test");

   278 writeln(term2str sc);

   279 "--- s1 ---";

   280 val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),req],_) =

   281 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

   283 val (_,_,_,_,_,dats,_) = StdinSML 1 1 ~1 ~1 (Command Auto);

   284 val FormKF (~16,Protect,0,Nundef,res) =

   285     (last_elem o drop_last o drop_last) dats;

   286 if res=(*"[]"*)"[x = -12 / 5]" then ()

   287 else raise error "new behaviour in test-example 2: [x =(-12)/5]";

   291 " ----------------- differentiate ----------------- ";

   292 " ----------------- d_d x (x ^^^ 2 + 3 * x + 4) ----------------- ";

   293 proofs:= []; dials:=([],[],[]);

   294 StdinSML 0 0 0 0 New_User;

   295 StdinSML 1 0 0 0 New_Proof;

   296 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",

   297 	   "differentiateFor x","derivative f_'_"];

   298 val (dI',pI',mI') =

   299   ("Diff.thy",["derivative_of","function"],

   300    ("Diff.thy","differentiate_on_R"));

   301 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

   302 (*FormKF (~10,Protect,0,Nundef,"#3 + #2 * x")*)

   303 (* 25.4.01: remove Error with NotAppl

   304  StdinSML 1 1 ~1  ~1 (RuleFK (Rewrite_Set "Test_simplify"));

   305  StdinSML 1 1 ~2  ~2 (RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_sum",""))));

   306  StdinSML 1 1 ~3  ~3 (RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_const",""))));

   307 uncaught exception TYPE ...

   309 val uI=1;val pI=1;val acI= ~3;val cI= ~3;

   310 val dat=(RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_const",""))));;

   311 *)

   314 (*18.4.01 tests mit speed*)

   316 StdinSML 1 1 ~1 ~1 (Command Accept);

   318 StdinSML 1 1 ~2 ~2 (Command SpeedPlus);

   319 StdinSML 1 1 ~2 ~2 (Command Accept);

   321 StdinSML 1 1 ~4 ~4 (Command SpeedMinus);

   322 StdinSML 1 1 ~4 ~4 (Command Accept);

   324 StdinSML 1 1 ~5 ~5 (Command Accept);

   325 (**)

   326 val xxx = StdinSML 1 1 ~6 ~6 (Command Auto);

   327 if xxx = ("@@@@@begin@@@@@",1,1,~6,[],

   328    [FormKF (~7,Protect,1,Nundef,"2 * x ^^^ (2 - 1) + 3 * d_d x x + 0"),

   329     FormKF (~8,Protect,1,Nundef,"2 * x ^^^ (2 - 1) + 3 * 1 + 0"),

   330     FormKF (~9,Protect,1,Nundef,"3 + 2 * x"),

   331     FormKF (~10,Protect,0,Nundef,"3 + 2 * x"),

   332     Request "start another example",End_Proof],"@@@@@end@@@@@")

   333 then () else writeln "new behaviour in example d_d x (x ^^^ 2 + 3 * x + 4), SpeedPlus/Minus";

   336 " ----------------- d_d x (x ^^^ 2 + x + 1 / x ^^^ 2) ----------------- ";

   337 proofs:= []; dials:=([],[],[]);

   338 StdinSML 0 0 0 0 New_User;

   339 StdinSML 1 0 0 0 New_Proof;

   340 val fmz = ["functionTerm (d_d x (x ^^^ 2 + x + 1 / x ^^^ 2))",

   341 	   "differentiateFor x","derivative f_'_"];

   342 val (dI',pI',mI') =

   343   ("Diff.thy",["derivative_of","function"],

   344    ("Diff.thy","differentiate_on_R"));

   345 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

   346 StdinSML 1 1 ~1 ~1 (Command Auto);

   347 (*FormKF (~12,Protect,0,Nundef,"#1 + (#2 * x + #-2 * x ^^^ #-3)")*)

   349 " ----------------- Schalk III S.62 Nr. 34a) --------- ";

   350 proofs:= []; dials:=([],[],[]);

   351 StdinSML 0 0 0 0 New_User;

   352 StdinSML 1 0 0 0 New_Proof;

   353 val fmz = ["functionTerm (d_d x ((5 * x ^^^ 2 - 2) * (7 * x + 1)))",

   354 	   "differentiateFor x","derivative f_'_"];

   355 val (dI',pI',mI') =

   356   ("Diff.thy",["derivative_of","function"],

   357    ("Diff.thy","differentiate_on_R"));

   358 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

   359 StdinSML 1 1 ~1 ~1 (Command Auto);

   362 " ----------------- Schalk III S.62 Nr. 51a) --------- ";

   363 proofs:= []; dials:=([],[],[]);

   364 StdinSML 0 0 0 0 New_User;

   365 StdinSML 1 0 0 0 New_Proof;

   366 val fmz = ["functionTerm (d_d x ((x+1)/(x- 1)))",

   367 	   "differentiateFor x","derivative f_'_"];

   368 val (dI',pI',mI') =

   369   ("Diff.thy",["derivative_of","function"],

   370    ("Diff.thy","differentiate_on_R"));

   371 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

   372 StdinSML 1 1 ~1 ~1 (Command Auto);

   373 (*"#-1 // (#1 + (x ^^^ #2 + #-2 * x)) +\n(x // (#1 + (x ^^^ #2 + #-2 * x)) +\n (#1 + x) * (#-1 // (#1 + (x ^^^ #2 + #-2 * x))))" ----- simplification !?!*)

   376 " ----------------- Schalk III S.144 Nr. 408b) --------- ";

   377 proofs:= []; dials:=([],[],[]);

   378 StdinSML 0 0 0 0 New_User;

   379 StdinSML 1 0 0 0 New_Proof;

   380 val fmz = ["functionTerm (d_d x (x ^^^ 2 * (ln ((sin x) ^^^ 2))))",

   381 	   "differentiateFor x","derivative f_'_"];

   382 val (dI',pI',mI') =

   383   ("Diff.thy",["derivative_of","function"],

   384    ("Diff.thy","differentiate_on_R"));

   385 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

   386 StdinSML 1 1 ~1 ~1 (Command Auto);

   387 (*"#2 * (x * ln (sin x ^^^ #2)) +\ncos x * (sin x * (x ^^^ #2 * (#2 // sin x ^^^ #2)))"---- cancel sin x !!!*)

   390 " ----------------- Schalk III S.137 Nr. 359g) --------- ";

   391 proofs:= []; dials:=([],[],[]);

   392 StdinSML 0 0 0 0 New_User;

   393 StdinSML 1 0 0 0 New_Proof;

   394 val fmz = ["functionTerm (d_d x (sqrt (cos (3*x))))",

   395 	   "differentiateFor x","derivative f_'_"];

   396 val (dI',pI',mI') =

   397   ("Diff.thy",["derivative_of","function"],

   398    ("Diff.thy","differentiate_on_R"));

   399 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));

   400 StdinSML 1 1 ~1 ~1 (Command Auto);

author	agriesma
	Thu, 17 Apr 2003 18:01:03 +0200
branch	griesmayer
changeset 338	90390fecbe74
child 709	f5b966aa0b4e
permissions	-rw-r--r--