1.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml	Thu Mar 17 10:11:18 2011 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml	Thu Mar 17 10:46:02 2011 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  (*apparently no way to do these tests within DiophantEq.thy:
     1.5  val thy = @{theory};(**** ME_Isa: thy 'DiophantEq' not in system
     1.6    from CalcTreeTest*)
     1.7 -(*(*val thy = @{theory "Isac"};toplevel error from store_met?!?*)*)
     1.8 +(*val thy = @{theory "Isac"};toplevel error from store_met?!?*)
     1.9  *)
    1.10  val thy = @{theory "DiophantEq"};
    1.11  val ctxt = ProofContext.init_global thy;
    1.12 @@ -36,7 +36,6 @@
    1.13  val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; 
    1.14  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
    1.15  
    1.16 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.17  "----------- mathengine with usecase1 -------------------";
    1.18  "----------- mathengine with usecase1 -------------------";
    1.19  "----------- mathengine with usecase1 -------------------";
    1.20 @@ -49,6 +48,7 @@
    1.21  "----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---";
    1.22  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.23  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.24 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.25  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.26  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.27  val (p,_,f,nxt,_,pt) = me nxt p c pt;