(* Title:  All tests on isac; observe outcommented

   Author: Walther Neuper 101001

   (c) copyright due to lincense terms.

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

$ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &

*)

theory Test_Isac imports Isac

uses 

  (         "library.sml")

  (         "calcelems.sml")

  ("ProgLang/termC.sml") 

  ("ProgLang/calculate.sml")

  ("ProgLang/rewrite.sml")

(*("ProgLang/listg.sml") ("ProgLang/scrtools.sml") ("ProgLang/tools.sml") *)

  ("Interpret/mstools.sml") 

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

  ("Interpret/ptyps.sml") 

(*("Interpret/generate.sml")*)

  ("Interpret/calchead.sml") 

(*("Interpret/appl.sml")*)

  ("Interpret/rewtools.sml") 

(*("Interpret/script.sml")

  ("Interpret/solve.sml") 

  ("Interpret/inform.sml")*)

  ("Interpret/mathengine.sml")

(*("xmlsrc/mathml.sml")

  ("xmlsrc/datatypes.sml")

  ("xmlsrc/pbl-met-hierarchy.sml")

  ("xmlsrc/thy-hierarchy.sml")*)

  ("xmlsrc/interface-xml.sml")

  ("Frontend/messages.sml")

  ("Frontend/states.sml")

  ("Frontend/interface.sml")

  ("print_exn_G.sml")

  ("Knowledge/delete.sml")

  ("Knowledge/descript.sml")

  ("Knowledge/atools.sml")

  ("Knowledge/simplify.sml")

  ("Knowledge/poly.sml")

  ("Knowledge/rational.sml")

  ("Knowledge/equation.sml")

  ("Knowledge/root.sml")

  ("Knowledge/lineq.sml")

  ("Knowledge/rooteq.sml")

  ("Knowledge/rateq.sml")

  ("Knowledge/rootrateq.sml")

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

  ("Knowledge/calculus.sml")

  ("Knowledge/trig.sml")

  ("Knowledge/logexp.sml")

  ("Knowledge/diff.sml")

  ("Knowledge/integrate.sml")

  ("Knowledge/eqsystem.sml")

  ("Knowledge/test.sml")

  ("Knowledge/polyminus.sml")

  ("Knowledge/vect.sml")

  ("Knowledge/diffapp.sml")

  ("Knowledge/biegelinie.sml")

  ("Knowledge/algein.sml")

  ("Knowledge/diophanteq.sml")

  ("Knowledge/isac.sml")

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 %%%%%%%%%%%%%%%%%%%%%";*}

  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 %%%%%%%%%%%%%%%%%%%%";*}

  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 %%%%%%%%%%%%%%%%%%%%%%%";*}

  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 %%%%%%%%%%%%%%%%%%%%%";*}

  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 %%%%%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}

end

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

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

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

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

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

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

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

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