(* 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/Isabelle/bin/isabelle jedit -l Isac Test_Isac.thy &

1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80         90      100

*)

theory Test_Isac imports 

  Isac

  "Knowledge/Rational_Test"

  "ADDTESTS/Ctxt"

uses 

  (         "library.sml")

  (         "calcelems.sml")

  ("ProgLang/termC.sml") 

  ("ProgLang/calculate.sml")

  ("ProgLang/rewrite.sml")

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

  ("Minisubpbl/000-comments.sml")

  ("Minisubpbl/100-init-rootpbl.sml")

  ("Minisubpbl/150-add-given.sml")

  ("Minisubpbl/200-start-method.sml")

  ("Minisubpbl/300-init-subpbl.sml")

  ("Minisubpbl/400-start-meth-subpbl.sml")

  ("Minisubpbl/500-postcond.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

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

  use "Minisubpbl/000-comments.sml"

  use "Minisubpbl/100-init-rootpbl.sml"

  use "Minisubpbl/150-add-given.sml"

  use "Minisubpbl/200-start-method.sml"

  use "Minisubpbl/300-init-subpbl.sml"

  use "Minisubpbl/400-start-meth-subpbl.sml"

  use "Minisubpbl/500-postcond.sml"

  ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*}

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

  use "Interpret/mstools.sml"       (*new 2010*)

  use "Interpret/ctree.sml"         (*!...see(25)*)

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

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

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

  use "Interpret/appl.sml"          (*!complete WEGEN INTERMED TESTCODE*)

  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.; diff.emacs--jedit*)

(*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/rlang.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

                                              diff.emacs--jedit*)

(*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 110503 ================================================

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

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

============ inhibit exn 110503 ==============================================*)

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

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