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

*)

theory Test_Isac imports

  "~~/src/Tools/isac/Frontend/Isac"

(*Isac

OUTCOMMENT THE ABOVE AND SET <Prover Session> <Isac> (INSTEAD OF 'HOL')*)

(*"Knowledge/Rational_Test" ...THIS FILE HAS DISAPPEARED*)

  "ADDTESTS/Ctxt"

  "ADDTESTS/test-depend/Build_Test"

  "ADDTESTS/All_Ctxt"

  "ADDTESTS/course/phst11/T1_Basics"

  "ADDTESTS/course/phst11/T2_Rewriting"

  "ADDTESTS/course/phst11/T3_MathEngine"

  "ADDTESTS/file-depend/Build_Test"

  "ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"

  "../../Pure/Isar/Test_Parsers"

(*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)

  "../../Pure/Isar/Test_Parse_Term"

uses 

  (         "library.sml")

  (         "calcelems.sml")

  ("ProgLang/termC.sml")      

  ("ProgLang/calculate.sml")

  ("ProgLang/rewrite.sml")

  ("ProgLang/listC.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/490-nxt-Check_Postcond.sml")

  ("Minisubpbl/500-met-sub-to-root.sml")

  ("Minisubpbl/530-error-Check_Elementwise.sml")

  ("Minisubpbl/600-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")

(*THIS WAITS UNTIL Isabelle2013: ("Knowledge/gcd_poly.sml") ("Knowledge/gcd_poly_winkler.sml")

  IN THIS SEQUENCE: SEE Test_Some2.thy*)

  ("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/partial_fractions.sml")

  ("Knowledge/polyminus.sml")

  ("Knowledge/vect.sml")

  ("Knowledge/diffapp.sml")

  ("Knowledge/biegelinie.sml")

  ("Knowledge/algein.sml")

  ("Knowledge/diophanteq.sml")

  ("Knowledge/Inverse_Z_Transform/inverse_z_transform.sml")

  ("Knowledge/isac.sml")

  ("Knowledge/build_thydata.sml")

begin

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

  use          "library.sml"

  use          "calcelems.sml"

  use "ProgLang/termC.sml"

  use "ProgLang/calculate.sml"

  use "ProgLang/rewrite.sml"

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

  use "ProgLang/scrtools.sml"

  use "ProgLang/tools.sml"

  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/490-nxt-Check_Postcond.sml"

  use "Minisubpbl/500-met-sub-to-root.sml"

  use "Minisubpbl/530-error-Check_Elementwise.sml"

  use "Minisubpbl/600-postcond.sml"

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

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

  use "Interpret/mstools.sml"

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

  use "Interpret/ptyps.sml"

  ML {* check_unsynchronized_ref (); (*========= on error: CUT AND PASTE THIS LINE =========*) *}

  use "Interpret/generate.sml"

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

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

  use "Interpret/rewtools.sml"      (*TODO/part.WN120406*)

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

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

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

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

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

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

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

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

  use "xmlsrc/pbl-met-hierarchy.sml" (*TODO after 2009-2/part.*)

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

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

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

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

  use "Frontend/messages.sml"

  use "Frontend/states.sml"

  use "Frontend/interface.sml"

  use          "print_exn_G.sml"

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

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

  use "Knowledge/delete.sml"

  use "Knowledge/descript.sml"

  use "Knowledge/atools.sml"

  use "Knowledge/simplify.sml"

  use "Knowledge/poly.sml"

(*THIS WAITS UNTIL Isabelle2013 IN THIS SEQUENCE (SEE Test_Some2.thy):0

  use "Knowledge/gcd_poly.sml" (*type error 'nth' etc*)

  use "Knowledge/gcd_poly_winkler.sml"*)

  use "Knowledge/gcd_poly.sml"

  use "Knowledge/gcd_poly_winkler.sml"

(*use "Knowledge/rational.sml"  WN120317.TODO postponed to joint work with dmeindl *)

  use "Knowledge/equation.sml"

  use "Knowledge/root.sml"

  use "Knowledge/lineq.sml"

(*use "Knowledge/rooteq.sml"    some complicated equations not recovered from 2002 *)

  use "Knowledge/rateq.sml"   (*some complicated equations not recovered from 2002 *)

  use "Knowledge/rootrat.sml"

  use "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)

  use "Knowledge/partial_fractions.sml"

  use "Knowledge/polyeq.sml"

(*use "Knowledge/rlang.sml"     much to clean up, not urgent due to similar tests  *)

  use "Knowledge/calculus.sml"

  use "Knowledge/trig.sml"

(*use "Knowledge/logexp.sml"    not included as stuff for presentation of authoring*) 

  use "Knowledge/diff.sml"

  use "Knowledge/integrate.sml"

  use "Knowledge/eqsystem.sml"

  use "Knowledge/test.sml"

  use "Knowledge/polyminus.sml"

  use "Knowledge/vect.sml"

  use "Knowledge/diffapp.sml"        (* postponed to dev. specification | TP-prog. *)

  use "Knowledge/biegelinie.sml"

  use "Knowledge/algein.sml"

  use "Knowledge/diophanteq.sml"

  use "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"

  use "Knowledge/isac.sml"

  use "Knowledge/build_thydata.sml"

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

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

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

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

end

(*========== inhibit exn 110628 ================================================

============ inhibit exn 110628 ==============================================*)

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

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