test/Tools/isac/Knowledge/system.sml
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37960 ec20007095f2
child 38031 460c24a6a6ba
equal deleted inserted replaced
37990:24609758d219 37991:028442673981
    45 "----------- me --------------------------------------------------";
    45 "----------- me --------------------------------------------------";
    46 "----------- me --------------------------------------------------";
    46 "----------- me --------------------------------------------------";
    47 val fmz = ["equalities [0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2, 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2]",
    47 val fmz = ["equalities [0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2, 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2]",
    48 	   "solveForVars [c, c_2]", "solution ss___"];
    48 	   "solveForVars [c, c_2]", "solution ss___"];
    49 val (dI',pI',mI') =
    49 val (dI',pI',mI') =
    50   ("Biegelinie.thy",["normalize","2x2","linear","system"],
    50   ("Biegelinie",["normalize","2x2","linear","system"],
    51    ["EqSystem","normalize","2x2"]);
    51    ["EqSystem","normalize","2x2"]);
    52 val p = e_pos'; val c = [];
    52 val p = e_pos'; val c = [];
    53 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    53 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    54 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
    54 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
    55 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
    55 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
    56 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    56 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    57 case nxt of (_, Specify_Theory "Biegelinie.thy") => ()
    57 case nxt of (_, Specify_Theory "Biegelinie") => ()
    58 	  | _ => raise error "system.sml diff.behav.in me --1";
    58 	  | _ => raise error "system.sml diff.behav.in me --1";
    59 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    59 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    60 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    60 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    61 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    61 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    62 case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
    62 case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
    65 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
    65 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
    66 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
    66 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
    67 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
    67 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
    68 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
    68 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
    69 
    69 
    70 case nxt of (_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", 
    70 case nxt of (_, Subproblem ("Biegelinie", ["triangular", "2x2", 
    71 					       "linear", "system"])) => ()
    71 					       "linear", "system"])) => ()
    72 	  | _ => raise error "system.sml diff.behav.in me --3";
    72 	  | _ => raise error "system.sml diff.behav.in me --3";
    73 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    73 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    74 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
    74 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
    75 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
    75 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
    76 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    76 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    77 case nxt of (_, Specify_Theory "Biegelinie.thy") => ()
    77 case nxt of (_, Specify_Theory "Biegelinie") => ()
    78 	  | _ => raise error "system.sml diff.behav.in me --1";
    78 	  | _ => raise error "system.sml diff.behav.in me --1";
    79 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    79 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    80 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    80 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    81 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    81 val (p,_,f,nxt,_,pt) = me nxt p c pt;
    82 case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
    82 case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()