test/Tools/isac/Test_Isac.thy
branchisac-update-Isa09-2
changeset 38010 a37a3ab989f4
parent 38009 b49723351533
child 38011 3147f2c1525c
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Tue Sep 14 12:12:42 2010 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Tue Sep 14 15:46:56 2010 +0200
     1.3 @@ -1,13 +1,15 @@
     1.4  (* Title Run_Tests on isac
     1.5  $ cd /usr/local/isabisac/test/Tools/isac
     1.6 -$ /usr/local/isabisac/bin/isabelle emacs Run_Tests.thy &
     1.7 +$ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
     1.8  
     1.9 +RESTART emacs after having created a new Isac heap.
    1.10  was sml/RTEST-root.sml in isac-2002
    1.11  *)
    1.12  
    1.13  theory Test_Isac imports Isac begin
    1.14   
    1.15  ML{* writeln "**** run the tests **************************************" *};
    1.16 +ML {* Toplevel.debug := true; *}
    1.17  (* 
    1.18  cd "systest";
    1.19  (*+ check kbtest/diffapp.sml for additional items in met-model*)
    1.20 @@ -60,7 +62,9 @@
    1.21   	use"complex.sml";
    1.22   	use"diff.sml";
    1.23   	use"diffapp.sml";
    1.24 -	use"integrate.sml";
    1.25 +*)
    1.26 +use"Knowledge/integrate.sml";
    1.27 +(*
    1.28  	use"equation.sml";
    1.29  	(*use"inssort.sml"; problems with recdef in Isabelle2002*)
    1.30   	use"logexp.sml";