(* Title: Run_Tests as long Isac is not available: REPLACE 'IMPORTS'

   Author: Walther Neuper 101001

   (c) copyright due to lincense terms.

$ cd /usr/local/isabisac/test/Tools/isac

$ /usr/local/isabisac/bin/isabelle emacs Test_Some.thy &

*)

theory Test_Isac imports Isac

  "ProgLang/ProgLang"

  "Interpret/Interpret"

  "xmlsrc/xmlsrc"

  "Frontend/Frontend"

  "Knowledge/Knowledge"

begin

(* cd "systest";

   (*+ check kbtest/diffapp.sml for additional items in met-model*)

       	use"root-equ.sml"; 

       	use"script.sml";   

	(* use"script_if.sml"; WN03 missing: is_rootequation_in*)

       	use"scriptnew.sml";     

       	use"subp-rooteq.sml";   

	use"tacis.sml";

	use"interface-xml.sml";

	(* use"testdaten.sml"; no update after dropping 'errorBound'*)

 	cd "../..";

*)

  ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}

  use "library.sml"                 (*new 2011*)

  use "calcelems.sml"               (*complete*)

  use "ProgLang/termC.sml"          (*part.*)

  use "ProgLang/calculate.sml"      (*part.*)

  use "ProgLang/rewrite.sml"        (*part.*)

(*use "ProgLang/listg.sml"            2002*)

(*use "ProgLang/scrtools.sml"         2002*)

(*use "ProgLang/tools.sml"            2002*)

  ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}

(*??? "ProgLang/ProgLang"*)

  ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}

  use "Interpret/mstools.sml"       (*empty*)

(*use "Interpret/ctree.sml"           TODO*)

  use "Interpret/ptyps.sml"         (*    *)

(*use "Interpret/generate.sml"        new 2011*)

  use "Interpret/calchead.sml"      (*    *)

(*use "Interpret/appl.sml"            new 2011*)

  use "Interpret/rewtools.sml"      (*    *)

(*use "Interpret/script.sml"          TODO*)

(*use "Interpret/solve.sml"           TODO*)

(*use "Interpret/inform.sml"          TODO*)

  use "Interpret/mathengine.sml"(*part.*)

  ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}

(*??? "Interpret/Interpret"*)

  ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}

(*use "xmlsrc/mathml.sml"             TODO*)

(*use "xmlsrc/datatypes.sml"          TODO*)

(*use "xmlsrc/pbl-met-hierarchy.sml"  TODO*)

(*use "xmlsrc/thy-hierarchy.sml"      TODO after 2009-2*) 

  use "xmlsrc/interface-xml.sml"    (*TODO after 2009-2*)

  ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}

(*??? "xmlsrc/xmlsrc"*)

  ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}

  use "Frontend/messages.sml"        (*new 2011*)

  use "Frontend/states.sml"          (*new 2011*)

  use "Frontend/interface.sml"       (*part.*)

  use "print_exn_G.sml"              (*new 2011*)

  ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}

(*??? "Frontend/Frontend"*)

  ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}

  use "Knowledge/delete.sml"         (*new 2011*)

  use "Knowledge/descript.sml"       (*new 2011*)

(*use "Knowledge/atools.sml"           2002, added termorder.sml 2011*)

  use "Knowledge/simplify.sml"       (*part.*)

(*use "Knowledge/poly.sml"             2002*)

  use "Knowledge/rational.sml"       (*part.*)

(*use "Knowledge/equation.sml"         2002*)

(*use "Knowledge/root.sml"             2002*)

  use "Knowledge/lineq.sml"          (*new 2011*)

(*use "Knowledge/rooteq.sml"           2002*)

(*use "Knowledge/rateq.sml"            2002*)

(*use "Knowledge/rootrat.sml"          2002*)

(*use "Knowledge/rootrateq.sml"        2002*)

(*use "Knowledge/polyeq.sml"           2002*)

  use "Knowledge/calculus.sml"       (*new 2011*)

(*use "Knowledge/trig.sml"             2002*)

(*use "Knowledge/logexp.sml"           2002*)

  use "Knowledge/diff.sml"           (*part.*)

  use "Knowledge/integrate.sml"      (*part. was complete 2009-2*)

(*use "Knowledge/eqsystem.sml"         2002*)

  use "Knowledge/test.sml"           (*new 2011*)

  use "Knowledge/polyminus.sml"      (*part.*)

(*use "Knowledge/vect.sml"             2002*)

(*use "Knowledge/diffapp.sml"          2002*)

(*use "Knowledge/biegelinie.sml"       2002*)

(*use "Knowledge/algein.sml"           2002*)

  use "Knowledge/diophanteq.sml"     (*complete*)

  use "Knowledge/isac.sml"           (*part.*)

  ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}

(*??? "Knowledge/Knowledge"*)

end

(*=== inhibit exn ?=============================================================

===== inhibit exn ?===========================================================*)

(*========== inhibit exn 110317 ================================================

"########### testcode inserted vvv ###########################################";

"########### testcode inserted ^^^ ###########################################";

============ inhibit exn 110317 ==============================================*)

(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)