test/Tools/isac/Minisubpbl/150-add-given.sml
author Walther Neuper <neuper@ist.tugraz.at>
Fri, 13 May 2011 09:28:38 +0200
branchdecompose-isar
changeset 41986 64efbbbed4b4
child 52070 77138c64f4f6
permissions -rw-r--r--
tuned
neuper@41986
     1
(* Title:  150-add-given.sml
neuper@41986
     2
   Author: Walther Neuper 1105
neuper@41986
     3
   (c) copyright due to lincense terms.
neuper@41986
     4
*)
neuper@41986
     5
neuper@41986
     6
val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
neuper@41986
     7
val (dI',pI',mI') =
neuper@41986
     8
  ("Test", ["sqroot-test","univariate","equation","test"],
neuper@41986
     9
   ["Test","squ-equ-test-subpbl1"]);
neuper@41986
    10
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = ("Model_Problem"*)
neuper@41986
    11
val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_,Add_Given "equality (x + 1 = 2)*)
neuper@41986
    12
val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = (_,Add_Given "solveFor x"*)
neuper@41986
    13
case nxt of (_, Add_Given "solveFor x") => ()
neuper@41986
    14
| _ => error "minisubpbl: Add_Given is broken in root-problem";
neuper@41986
    15