src/Tools/isac/Test_Isac.thy
branchisac-update-Isa09-2
changeset 38056 98ebf8c25a28
parent 38055 e9ee52ea1454
child 38057 293a30867f15
equal deleted inserted replaced
38055:e9ee52ea1454 38056:98ebf8c25a28
    64  	use"datatypes.sml";        
    64  	use"datatypes.sml";        
    65        	use"pbl-met-hierarchy.sml"; 
    65        	use"pbl-met-hierarchy.sml"; 
    66        	use"thy-hierarchy.sml"; 
    66        	use"thy-hierarchy.sml"; 
    67  	cd "../.."; 
    67  	cd "../.."; 
    68 cd"smltest/FE-interface";
    68 cd"smltest/FE-interface";
    69        	use"interface.sml";
    69 *)
       
    70 use"../../../test/Tools/isac/Frontend/interface.sml"; (**)
       
    71 (*
    70  	cd "../..";
    72  	cd "../..";
    71 *)
    73 *)
    72 ML{* writeln "**** run tests on math-engine complete ******************" *};
    74 ML{* writeln "**** run tests on math-engine complete ******************" *};
    73 (*
    75 (*
    74 cd"smltest/IsacKnowledge"; ---below the order as in theoryy Isac---
    76 cd"smltest/IsacKnowledge"; ---below the order as in theoryy Isac---
    92 	use"wn.sml";
    94 	use"wn.sml";
    93  	use"trig.sml";
    95  	use"trig.sml";
    94  	use"logexp.sml";
    96  	use"logexp.sml";
    95  	use"diff.sml";
    97  	use"diff.sml";
    96 *)
    98 *)
    97 use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*part.*)
    99 use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*all done*)
    98 
       
    99 ML {*111*}
       
   100 
       
   101 (*
   100 (*
   102 	use"eqsystem.sml";
   101 	use"eqsystem.sml";
   103 *)
   102 *)
   104 use "../../../test/Tools/isac/Knowledge/polyminus.sml"; (*part.*)
   103 use "../../../test/Tools/isac/Knowledge/polyminus.sml"; (*part.*)
   105 (*
   104 (*
   146 end
   145 end
   147 
   146 
   148 (*=== inhibit exn ?=============================================================
   147 (*=== inhibit exn ?=============================================================
   149 ===== inhibit exn ?===========================================================*)
   148 ===== inhibit exn ?===========================================================*)
   150 
   149 
       
   150 
   151 (*========== inhibit exn =======================================================
   151 (*========== inhibit exn =======================================================
       
   152 
       
   153 "########### testcode inserted vvv ###########################################";
       
   154 "########### testcode inserted ^^^ ###########################################";
       
   155 
   152 ============ inhibit exn =====================================================*)
   156 ============ inhibit exn =====================================================*)
       
   157 
   153 
   158 
   154 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
   159 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
   155 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
   160 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)