test/Tools/isac/Knowledge/diophanteq.sml
branchdecompose-isar
changeset 42166 911c49949ba9
parent 41951 50bc995aa45b
child 48761 4162c4f6f897
     1.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml	Thu Jul 21 12:01:56 2011 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml	Fri Jul 22 14:01:09 2011 +0200
     1.3 @@ -53,14 +53,12 @@
     1.4      ["Test", "solve_diophant"]));
     1.5  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];
     1.6  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
     1.7 -(*========== inhibit exn WN110318 ==============================================
     1.8  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
     1.9  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.10  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.11  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.12  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.13  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.14 -============ inhibit exn WN110318 ============================================*)
    1.15  
    1.16  "----------- rewriting for usecase2 ---------------------";
    1.17  "----------- rewriting for usecase2 ---------------------";
    1.18 @@ -100,5 +98,4 @@
    1.19  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.20  (*nxt = ("Empty_Tac", ...) #############################*)
    1.21  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.22 -(*========== inhibit exn WN110318 ==============================================
    1.23 -============ inhibit exn WN110318 ============================================*)
    1.24 +