1.1 --- a/test/Tools/isac/Test_Isac.thy	Tue May 17 09:55:30 2011 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Tue May 17 14:56:54 2011 +0200
     1.3 @@ -98,8 +98,41 @@
     1.4    use "Minisubpbl/150-add-given.sml"
     1.5    use "Minisubpbl/200-start-method.sml"
     1.6    use "Minisubpbl/300-init-subpbl.sml"
     1.7 +  use "Minisubpbl/400-start-meth-subpbl.sml"
     1.8 +  use "Minisubpbl/500-postcond.sml"
     1.9 +
    1.10  ML {*
    1.11 -
    1.12 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    1.13 +val (dI',pI',mI') =
    1.14 +   ("Test", ["sqroot-test","univariate","equation","test"],
    1.15 +    ["Test","squ-equ-test-subpbl1"]);
    1.16 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.17 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.18 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.19 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.20 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.21 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.22 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.23 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
    1.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.30 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.31 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.33 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.34 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.35 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
    1.36 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
    1.37 +*}
    1.38 +ML {*
    1.39 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
    1.40 +*}
    1.41 +ML {*
    1.42 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.43  *}
    1.44  ML {*
    1.45  *}
    1.46 @@ -107,12 +140,8 @@
    1.47  *}
    1.48  ML {*
    1.49  *}
    1.50 -ML {*
    1.51 -*}
    1.52 -ML {*
    1.53 -*}
    1.54 -  use "Minisubpbl/400-start-meth-subpbl.sml"
    1.55 -  use "Minisubpbl/500-postcond.sml"
    1.56 +
    1.57 +
    1.58    ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*}
    1.59    ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
    1.60    use "Interpret/mstools.sml"       (*new 2010*)
    1.61 @@ -188,11 +217,25 @@
    1.62  insert_assumptions am
    1.63  *}
    1.64  ML {*
    1.65 -get_ctxt pt p |> insert_assumptions am
    1.66 +val ctxt = get_ctxt pt p |> insert_assumptions am
    1.67  *}
    1.68  ML {*
    1.69  from_pblobj_or_detail'
    1.70  *}
    1.71 +ML {*
    1.72 +from_pblobj'
    1.73 +*}
    1.74 +ML {*
    1.75 +*}
    1.76 +ML {*
    1.77 +*}
    1.78 +ML {*
    1.79 +*}
    1.80 +ML {*
    1.81 +*}
    1.82 +ML {*
    1.83 +*}
    1.84 +
    1.85  end
    1.86  
    1.87  (*=== inhibit exn ?=============================================================