1.1 --- a/test/Tools/isac/Test_Isac.thy	Sat Jun 18 11:28:10 2011 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Jun 20 17:33:06 2011 +0200
     1.3 @@ -12,7 +12,15 @@
     1.4    Isac
     1.5    "Knowledge/Rational_Test"
     1.6    "ADDTESTS/Ctxt"
     1.7 +  "ADDTESTS/test-depend/Build_Test"
     1.8    "ADDTESTS/All_Ctxt"
     1.9 +(*"ADDTESTS/course/T2_Rewriting" theory has not been declared*)
    1.10 +(*"ADDTESTS/course/T1_Basics.thy" could not find ^^^*)
    1.11 +(*"ADDTESTS/course/T3_MathEngine" could not find ^^^*)
    1.12 +  "ADDTESTS/file-depend/Build_Test"
    1.13 +  "../../Pure/Isar/Test_Parsers"
    1.14 +(*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)
    1.15 +  "../../Pure/Isar/Test_Parse_Term"
    1.16   
    1.17  uses 
    1.18    (         "library.sml")
    1.19 @@ -131,7 +139,23 @@
    1.20    ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
    1.21    use "Frontend/messages.sml"        (*new 2011*)
    1.22    use "Frontend/states.sml"          (*new 2011*)
    1.23 -  use "Frontend/interface.sml"       (*part.*)                            
    1.24 +  use "Frontend/interface.sml"       (*part.*)
    1.25 +ML {*
    1.26 +
    1.27 +*}
    1.28 +ML {*
    1.29 +
    1.30 +*}
    1.31 +ML {*
    1.32 +
    1.33 +*}
    1.34 +ML {*
    1.35 +
    1.36 +*}
    1.37 +ML {*
    1.38 +
    1.39 +*}
    1.40 +                            
    1.41    use         "print_exn_G.sml"      (*new 2011*)
    1.42    ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
    1.43    ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
    1.44 @@ -171,11 +195,16 @@
    1.45    ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
    1.46  
    1.47  ML {*
    1.48 -*}
    1.49 -ML {*
    1.50 -*}
    1.51 -  ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
    1.52 -ML {*
    1.53 +"--------- mini-subpbl AUTO CompleteCalcHead ------------";
    1.54 + states:=[];
    1.55 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
    1.56 +   ("Test", ["sqroot-test","univariate","equation","test"],
    1.57 +    ["Test","squ-equ-test-subpbl1"]))];
    1.58 + Iterator 1;
    1.59 + moveActiveRoot 1;
    1.60 +(* doesn't terminate !!!*)
    1.61 + autoCalculate 1 CompleteCalcHead; 
    1.62 +val (ModSpec (x1,x2,x3,x4,x5,x6), tac, asms) =  pt_extract (pt, p);
    1.63  *}
    1.64  ML {*
    1.65  *}
    1.66 @@ -183,20 +212,19 @@
    1.67  *}
    1.68  ML {*
    1.69  *}
    1.70 -ML {*
    1.71 -*}
    1.72 +  ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
    1.73  
    1.74  end
    1.75  
    1.76  (*=== inhibit exn ?=============================================================
    1.77  ===== inhibit exn ?===========================================================*)
    1.78  
    1.79 -(*========== inhibit exn 110520 ================================================
    1.80 +(*========== inhibit exn 110620 ================================================
    1.81  
    1.82  "########### testcode inserted vvv ###########################################";
    1.83  "########### testcode inserted ^^^ ###########################################";
    1.84  
    1.85 -============ inhibit exn 110520 ==============================================*)
    1.86 +============ inhibit exn 110620 ==============================================*)
    1.87  
    1.88  (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.89  -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)