
walther@59963: t(* Title:  All tests on isac (some outcommented since Isabelle2002-->2009-2)
wneuper@59553:    Author: Walther Neuper 101001
wneuper@59553:    (c) copyright due to license terms.
wneuper@59553: 
wneuper@59553:    Isac's tests are organised parallel to sources: 
wneuper@59553:      "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
wneuper@59553:    plus
wneuper@59553:      ~~/test/Tools/isac/ADDTESTS
wneuper@59553:      ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
walther@59935: 
walther@59935: Note, that only the first error in a file is shown here.
wneuper@59553: *)
wneuper@59553: 
walther@59623: section \<open>Notes on running tests\<close>
walther@59623: subsection \<open>Switch between running tests and updating code\<close>
wneuper@59553: text \<open>
walther@59623:   Isac encapsulates code as much as possible in structures without open.
walther@59623:   This policy conflicts with those tests, which go into functions to details
walther@59623:   not declared in the signatures.
walther@59623:   
walther@59623:   In order to maintain these tests without changes, this has to be done before running tests:
walther@59623:   (1) Extend signatures for tests by
walther@59623:       ~~$ ./xcoding-to-test.sh
walther@59623:       ~~$ ./zcoding-to-test.sh  # --"-- + go back to Test_Isac.thy
walther@59623:       Running Test_Isac.thy opens all structures, see code after "begin" below.
walther@59623:   (2) Clean signatures for coding
walther@59623:       ~~$ ./xtest-to-coding.sh
walther@59623:       ~~$ ./ztest-to-coding.sh  # --"-- + go back to coding (!update thy!)
wneuper@59553: 
walther@59964: //******************* don't forget (2) BEFORE pushing to repository **************************\\
walther@59623: \<close>
walther@59623: subsection \<open>Decide between running Test_Isac_Short.thy and Test_Isac.thy\<close>
walther@59623: text \<open>
walther@59623:   Some tests raise exception Size raised (line 171 of "./basis/LibrarySupport.sml")
walther@59623:   if run in x86_64_32 mode of Poly/ML 5.8 (which is set as default).
walther@59626:   This exception can be avoided by ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.
walther@59626:   A model is in the repository at ~~/etc/preferences.
walther@59623:   These preferences have drawbacks, however:
walther@59623:   * they claim more memory such that Isabelle instances canNOT run in parallel.
walther@59623:   * they do NOT reach Build_Isac.thy hanging in Build_Thydata.thy, see there.
wneuper@59553: 
walther@59623:   So default for Build_Isac.thy and for general testing is Test_Isac_Short.thy is x86_64_32 mode.
walther@59623:   From time to time full testing in Test_Isac.thy is recommended. For that purpose
walther@59626:   * set ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.
wneuper@59553: 
walther@59964: \\******************* don't forget to re-set defaults BEFORE updating code *******************//
walther@59623: 
walther@59626:     Note that Isabelle/jEdit re-generates the preferences file on shutdown, thus always use
walther@59626:     ***************** $ gedit ~/.isabelle/isabisac/etc/preferences &
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: section \<open>Run the tests\<close>
wneuper@59553: text \<open>
wneuper@59553: * say "OK" to the popup asking for theories to be loaded
wneuper@59553: * watch the <Theories> window for errors in the "imports" below
wneuper@59553: \<close>
wneuper@59553: 
walther@59623: theory Test_Isac_Short
walther@59603:   imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)
walther@59964:   (* in case the imports below raise ERROR, open each theory one by one *)
wneuper@59553: (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
walther@59964:   "~~/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All"
walther@59964:   "~~/test/Tools/isac/ADDTESTS/Ctxt"
walther@59964:   "~~/test/Tools/isac/ADDTESTS/test-depend/Build_Test"
walther@59964:   "~~/test/Tools/isac/ADDTESTS/All_Ctxt"
walther@59964:   "~~/test/Tools/isac/ADDTESTS/Test_Units"
walther@59964:   "~~/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
walther@59964:   "~~/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
walther@59964:   "~~/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
walther@59964:   "~~/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
walther@59964:   "~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo"
wneuper@59553: (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
wneuper@59553:    ADDTESTS/------------------------------------------- see end of tests *)
wneuper@59553: (*"~~/test/Pure/Isar/Test_Parsers"           dropped Isabelle2014-->2015 *)
wneuper@59553: (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
wneuper@59553:   "~~/test/Pure/Isar/Test_Parse_Term"
wneuper@59553: (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
wneuper@59553:   "~~/test/Tools/isac/Interpret/ptyps"       (* setup for ptyps.sml    *)
walther@59902:   "~~/test/Tools/isac/ProgLang/calculate"    (* setup for evaluate.sml*)
wneuper@59553:   "~~/test/Tools/isac/Knowledge/integrate"   (* setup for integrate.sml*)
wneuper@59553: (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
wneuper@59556: (*"~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)        Test_Isac_Short*)
wneuper@59556: (*"~~/src/Tools/isac/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)        Test_Isac_Short*)
wneuper@59556: (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
wneuper@59553: 
wneuper@59553: begin
wneuper@59553: 
walther@59628: ML \<open>open ML_System\<close>
wneuper@59553: ML \<open>
wneuper@59553: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
wneuper@59553:                       (* these vvv test, if funs are intermediately opened in structure 
walther@59628:                          in case of errors here consider ~~/xtest-to-coding.sh      *)
wneuper@59553:   open Kernel;
walther@59814:   open Math_Engine;
walther@59814:   open Test_Code;              CalcTreeTEST;
walther@59848:   open LItool;                 arguments_from_model;
walther@59817:   open Sub_Problem;
walther@59823:   open Fetch_Tacs;
walther@59814:   open Step
walther@59659:   open Env;
walther@59814:   open LI;                     scan_dn;
walther@59617:   open Istate;
walther@59909:   open Error_Pattern;
walther@59909:   open Error_Pattern_Def;
walther@59822:   open In_Chead;
wneuper@59553:   open Chead;                  pt_extract;
wneuper@59553:   open Ctree;                  append_problem;
walther@59696:   open Pos;
walther@59618:   open Program;
wneuper@59601:   open Prog_Tac;
walther@59603:   open Tactical;
walther@59603:   open Prog_Expr;
walther@59618:   open Auto_Prog;              rule2stac;
wneuper@59600:   open Input_Descript;
wneuper@59553:   open Specify;                show_ptyps;
walther@59763:   open SpecifyNEW;
walther@59763:   open Step_Specify;
walther@59749:   open Step_Solve;
walther@59763:   open Step;
wneuper@59553:   open Solve;                  (* NONE *)
wneuper@59577:   open Stool;                  (* NONE *)
wneuper@59577:   open ContextC;               transfer_asms_from_to;
walther@59814:   open Tactic;                 (* NONE *)
walther@59959:   open P_Model;                  (* NONE *)
walther@59872:   open Rewrite;
walther@59878:   open Eval;                   get_pair;
wneuper@59553:   open TermC;                  atomt;
walther@59858:   open Rule;
walther@59878:   open Rule_Set;               Sequence;
walther@59919:   open Eval_Def
walther@59854:   open ThyC
walther@59865:   open ThmC_Def
walther@59858:   open ThmC
walther@59857:   open Rewrite_Ord
walther@59861:   open UnparseC
wneuper@59553: (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: ML \<open>
walther@59659: "~~~~~ fun xxx , args:"; val () = ();
walther@59659: "~~~~~ and xxx , args:"; val () = ();
walther@59814: "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
walther@59814: (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return from xxx*);
walther@59659: "xx"
walther@59814: ^ "xxx"   (*+*) (*!for return!*) (*isa*) (*REP*) (**)
walther@59723: \<close> ML \<open>
walther@59723: \<close>
walther@59723: ML \<open>
walther@59723: \<close> ML \<open>
wneuper@59553: \<close> ML \<open>
walther@59851: \<close> ML \<open>
walther@59851: \<close> ML \<open>
walther@59892: \<close> ML \<open>
walther@59892: \<close> ML \<open>
walther@59851: \<close> ML \<open>
walther@59851: \<close> ML \<open>
walther@59851: \<close> ML \<open>
walther@59851: \<close> ML \<open>
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: ML \<open>
wneuper@59553:   KEStore_Elems.set_ref_thy @{theory};
wneuper@59553:   (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: (*---------------------- check test file by testfile -------------------------------------------
wneuper@59553:   ---------------------- check test file by testfile -------------------------------------------*)
wneuper@59553: section \<open>trials with Isabelle's functions\<close>
wneuper@59553:   ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
wneuper@59553:   ML_file "~~/test/Pure/General/alist.ML"
wneuper@59553:   ML_file "~~/test/Pure/General/basics.ML"
wneuper@59553:   ML_file "~~/test/Pure/General/scan.ML"
wneuper@59553:   ML_file "~~/test/Pure/PIDE/xml.ML"
wneuper@59553:   ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
wneuper@59553: 
wneuper@59553: section \<open>test ML Code of isac\<close>
wneuper@59600: subsection \<open>basic code first\<close>
wneuper@59553:   ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
walther@59866:   ML_file "BaseDefinitions/libraryC.sml"
walther@59866:   ML_file "BaseDefinitions/rule-def.sml"
walther@59919:   ML_file "BaseDefinitions/eval-def.sml"
walther@59866:   ML_file "BaseDefinitions/rewrite-order.sml"
walther@59866:   ML_file "BaseDefinitions/theoryC.sml"
walther@59866:   ML_file "BaseDefinitions/rule.sml"
walther@59866:   ML_file "BaseDefinitions/thmC-def.sml"
walther@59866:   ML_file "BaseDefinitions/error-fill-def.sml"
walther@59866:   ML_file "BaseDefinitions/rule-set.sml"
walther@59892:   ML_file "BaseDefinitions/check-unique.sml"
walther@59932: (*called by Know_Store..*)
walther@59866:   ML_file "BaseDefinitions/calcelems.sml"
walther@59866:   ML_file "BaseDefinitions/termC.sml"
walther@59912:   ML_file "BaseDefinitions/substitution.sml"
walther@59866:   ML_file "BaseDefinitions/contextC.sml"
walther@59866:   ML_file "BaseDefinitions/environment.sml"
walther@59964:   ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
wneuper@59553: (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
wneuper@59553:   ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
walther@59932: 
walther@59964:   ML_file "ProgLang/evaluate.sml"       (* requires setup from calculate.thy                    *)
walther@59633:   ML_file "ProgLang/listC.sml"
walther@59633:   ML_file "ProgLang/prog_expr.sml"
walther@59633:   ML_file "ProgLang/program.sml"
walther@59633:   ML_file "ProgLang/prog_tac.sml"
walther@59763:   ML_file "ProgLang/tactical.sml"
walther@59633:   ML_file "ProgLang/auto_prog.sml"
wneuper@59553: (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
wneuper@59553:   ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
wneuper@59600: 
wneuper@59600: subsection \<open>basic functionality on simple example first\<close>
wneuper@59553:   ML_file "Minisubpbl/000-comments.sml"
wneuper@59553:   ML_file "Minisubpbl/100-init-rootpbl.sml"
wneuper@59553:   ML_file "Minisubpbl/150-add-given.sml"
walther@59781:   ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"
wneuper@59553:   ML_file "Minisubpbl/200-start-method.sml"
wneuper@59553:   ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
walther@59722:   ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
wneuper@59553:   ML_file "Minisubpbl/300-init-subpbl.sml"
wneuper@59553:   ML_file "Minisubpbl/400-start-meth-subpbl.sml"
wneuper@59553:   ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml"
walther@59722:   ML_file "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
wneuper@59553:   ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
wneuper@59553:   ML_file "Minisubpbl/500-met-sub-to-root.sml"
wneuper@59553:   ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
walther@59781:   ML_file "Minisubpbl/600-postcond-NEXT_STEP.sml"
wneuper@59553:   ML_file "Minisubpbl/600-postcond.sml"
wneuper@59553:   ML_file "Minisubpbl/700-interSteps.sml"
walther@59820:   ML_file "Minisubpbl/710-interSteps-short.sml"
walther@59836:   ML_file "Minisubpbl/790-complete-NEXT_STEP.sml"
walther@59686:   ML_file "Minisubpbl/790-complete.sml"
walther@59813:   ML_file "Minisubpbl/800-append-on-Frm.sml"
wneuper@59600: 
wneuper@59600: subsection \<open>further functionality alongside batch build sequence\<close>
walther@59865:   ML_file "MathEngBasic/thmC.sml"
walther@59865:   ML_file "MathEngBasic/rewrite.sml"
walther@59674:   ML_file "MathEngBasic/mstools.sml"
walther@59728:   ML_file "MathEngBasic/tactic.sml"
walther@59774:   ML_file "MathEngBasic/ctree.sml"
walther@59774:   ML_file "MathEngBasic/calculation.sml"
walther@59763: 
walther@59952:   ML_file "Specify/o-model.sml"
walther@59957:   ML_file "Specify/i-model.sml"
wneuper@59594:   ML_file "Specify/ptyps.sml"         (* requires setup from ptyps.thy *)
wneuper@59553:   ML \<open>(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\<close>
wneuper@59594:   ML_file "Specify/calchead.sml"
walther@59800:   ML_file "Specify/step-specify.sml"
walther@59763:   ML_file "Specify/specify.sml"
walther@59813: 
walther@59860:   ML_file "Interpret/istate.sml"
walther@59817:   ML_file "Interpret/sub-problem.sml"
walther@59909:   ML_file "Interpret/error-pattern.sml"
walther@59790:   ML_file "Interpret/li-tool.sml"
wneuper@59561:   ML_file "Interpret/lucas-interpreter.sml"
walther@59751:   ML_file "Interpret/step-solve.sml"
walther@59751: 
walther@59823:   ML_file "MathEngine/fetch-tactics.sml"
wneuper@59600:   ML_file "MathEngine/solve.sml"
walther@59763:   ML_file "MathEngine/step.sml"
wneuper@59600:   ML_file "MathEngine/mathengine-stateless.sml"    (*!part. WN130804: +check Interpret/me.sml*)
wneuper@59600:   ML_file "MathEngine/messages.sml"
wneuper@59600:   ML_file "MathEngine/states.sml"
wneuper@59600: 
walther@59917:   ML_file "BridgeLibisabelle/thy-present.sml"
wneuper@59600:   ML_file "BridgeLibisabelle/mathml.sml"           (*part.*)
wneuper@59600:   ML_file "BridgeLibisabelle/datatypes.sml"        (*TODO/part.*)
wneuper@59600:   ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
wneuper@59600:   ML_file "BridgeLibisabelle/thy-hierarchy.sml"
wneuper@59600:   ML_file "BridgeLibisabelle/interface-xml.sml"     (*TODO after 2009-2*)
wneuper@59600:   ML_file "BridgeLibisabelle/interface.sml"
wneuper@59553: (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
wneuper@59553:   ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
wneuper@59600: 
wneuper@59553:   ML_file "Knowledge/delete.sml"
wneuper@59553:   ML_file "Knowledge/descript.sml"
wneuper@59553:   ML_file "Knowledge/simplify.sml"
wneuper@59553:   ML_file "Knowledge/poly.sml"
wneuper@59553:   ML_file "Knowledge/gcd_poly_ml.sml"
wneuper@59553:   ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
wneuper@59556: (*ML_file "Knowledge/rational.sml"                                              Test_Isac_Short*)
wneuper@59553:   ML_file "Knowledge/equation.sml"
wneuper@59553:   ML_file "Knowledge/root.sml"
wneuper@59553:   ML_file "Knowledge/lineq.sml"
wneuper@59553: (*ML_file "Knowledge/rooteq.sml"    some complicated equations not recovered from 2002 *)
walther@59628: (*ML_file "Knowledge/rateq.sml"     some complicated equations not recovered----Test_Isac_Short*)
wneuper@59553:   ML_file "Knowledge/rootrat.sml"
wneuper@59553:   ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
walther@59628: (*ML_file "Knowledge/partial_fractions.sml"  hangs with ML_system_64 = "true"---Test_Isac_Short*)
walther@59628:   ML_file "Knowledge/polyeq-1.sml"
walther@59636: (*ML_file "Knowledge/polyeq-2.sml"                                              Test_Isac_Short*)
wneuper@59553: (*ML_file "Knowledge/rlang.sml"     much to clean up, similar tests in other files     *)
wneuper@59553:   ML_file "Knowledge/calculus.sml"
wneuper@59553:   ML_file "Knowledge/trig.sml"
wneuper@59553: (*ML_file "Knowledge/logexp.sml"    not included as stuff for presentation of authoring*) 
wneuper@59553:   ML_file "Knowledge/diff.sml"
wneuper@59553:   ML_file "Knowledge/integrate.sml"
wneuper@59553:   ML_file "Knowledge/eqsystem.sml"
walther@59833:   ML_file "Knowledge/test.sml"                                                                                                     
wneuper@59553:   ML_file "Knowledge/polyminus.sml"
wneuper@59553:   ML_file "Knowledge/vect.sml"
wneuper@59553:   ML_file "Knowledge/diffapp.sml"        (* postponed to dev. specification | TP-prog. *)
walther@59623:   ML_file "Knowledge/biegelinie-1.sml"
walther@59628: (*ML_file "Knowledge/biegelinie-2.sml"                                          Test_Isac_Short*)
walther@59628: (*ML_file "Knowledge/biegelinie-3.sml"                                          Test_Isac_Short*)
walther@59628: (*ML_file "Knowledge/biegelinie-4.sml"       hangs with ML_system_64 = "true"---Test_Isac_Short*)
wneuper@59553:   ML_file "Knowledge/algein.sml"
wneuper@59553:   ML_file "Knowledge/diophanteq.sml"
walther@59628: (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)
wneuper@59553:   ML_file "Knowledge/inssort.sml"
wneuper@59553:   ML_file "Knowledge/isac.sml"
wneuper@59553:   ML_file "Knowledge/build_thydata.sml"
wneuper@59600: 
walther@59814:   ML_file "Test_Code/test-code.sml"
walther@59814: 
walther@59617: section \<open>further tests additional to src/.. files\<close>
wneuper@59600:   ML_file "BridgeLibisabelle/use-cases.sml"
wneuper@59553:   ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
wneuper@59553:   ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
wneuper@59600: 
wneuper@59553:   ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
wneuper@59553:   ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
wneuper@59553:   ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
wneuper@59561: ML \<open>
wneuper@59561: \<close> ML \<open>
wneuper@59561: \<close> ML \<open>
walther@59804: \<close> ML \<open>
walther@59804: \<close> ML \<open>
walther@59804: \<close> ML \<open>
walther@59804: \<close> ML \<open>
walther@59804: \<close> ML \<open>
walther@59804: \<close> ML \<open>
walther@59804: \<close> ML \<open>
walther@59804: \<close> ML \<open>
wneuper@59561: \<close>
wneuper@59553: 
wneuper@59553: section \<open>history of tests\<close>
wneuper@59553: text \<open>
wneuper@59553:   Systematic regression tests have been introduced to isac development in 2003.
wneuper@59553:   Sanity of the regression tests suffers from updates following Isabelle development,
wneuper@59553:   which mostly exceeded the resources available in isac's development.
wneuper@59553: 
wneuper@59553:   The survey below shall support to efficiently use the tests for isac 
wneuper@59553:   on different Isabelle versions. Conclusion in most cases will be: 
wneuper@59553: 
wneuper@59553:   !!! Use most recent tests or go back to the old notebook
wneuper@59553:       with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: 
wneuper@59553: subsection \<open>isac on Isabelle2017\<close>
wneuper@59553: subsubsection \<open>Summary of development\<close>
wneuper@59553: text \<open>
wneuper@59553:   * Add further signatures, separate structures and cleanup respective files.
wneuper@59553:   * Show feasibility of moving Isac programs to partial_function, i.e. to the function package.
wneuper@59553:   * Clean theory dependencies.
wneuper@59553:   * Start preparing shift from isac-java to Isabelle/jEdit.
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>State of tests: unchanged\<close>
wneuper@59553: subsubsection \<open>Changesets of begin and end\<close>
wneuper@59553: text \<open>
wneuper@59553:   last changeset with Test_Isac 925fef0f4c81
wneuper@59553:   first changeset with Test_Isac bbb414976dfe
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: subsection \<open>isac on Isabelle2015\<close>
wneuper@59553: subsubsection \<open>Summary of development\<close>
wneuper@59553: text \<open>
wneuper@59553:   * Add signatures from top of thy-hierarchy down to Interpret (not ProgLang).
wneuper@59553:     This complicates Test_Isac, see "Prepare running tests" above.
wneuper@59553:   * Remove TTY interface.
wneuper@59553:   * Re-activate insertion sort.
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>State of tests: unchanged\<close>
wneuper@59553: subsubsection \<open>Changesets of begin and end\<close>
wneuper@59553: text \<open>
wneuper@59553:   last changeset with Test_Isac 2f1b2854927a
wneuper@59553:   first changeset with Test_Isac ???
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: subsection \<open>isac on Isabelle2014\<close>
wneuper@59553: subsubsection \<open>Summary of development\<close>
wneuper@59553: text \<open>
wneuper@59553:   migration from "isabelle tty" --> libisabelle
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: subsection \<open>isac on Isabelle2013-2\<close>
wneuper@59553: subsubsection \<open>Summary of development\<close>
wneuper@59553: text \<open>
wneuper@59553:   reactivated context_thy
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>State of tests\<close>
wneuper@59553: text \<open>
wneuper@59553:   TODO
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>Changesets of begin and end\<close>
wneuper@59553: text \<open>
wneuper@59553:   TODO
wneuper@59553:   :
wneuper@59553:   : isac on Isablle2013-2
wneuper@59553:   :
wneuper@59553:   Changeset: 55318 (03826ceb24da) merged
wneuper@59553:   User: Walther Neuper <neuper@ist.tugraz.at>
wneuper@59553:   Date: 2013-12-12 14:27:37 +0100 (7 minutes)
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: subsection \<open>isac on Isabelle2013-1\<close>
wneuper@59553: subsubsection \<open>Summary of development\<close>
wneuper@59553: text \<open>
wneuper@59553:   Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
wneuper@59553:   no significant development steps for ISAC.
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>State of tests\<close>
wneuper@59553: text \<open>
wneuper@59553:   See points in subsection "isac on Isabelle2011", "State of tests".
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>Changesets of begin and end\<close>
wneuper@59553: text \<open>
wneuper@59553:   Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
wneuper@59553:   User: Walther Neuper <neuper@ist.tugraz.at>
wneuper@59553:   Date: 2013-12-03 18:13:31 +0100 (8 days)
wneuper@59553:   :
wneuper@59553:   : isac on Isablle2013-1
wneuper@59553:   :
wneuper@59553:   Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
wneuper@59553:   User: Walther Neuper <neuper@ist.tugraz.at>
wneuper@59553:   Date: 2013-11-21 18:12:17 +0100 (2 weeks)
wneuper@59553: 
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: subsection \<open>isac on Isabelle2013\<close>
wneuper@59553: subsubsection \<open>Summary of development\<close>
wneuper@59553: text \<open>
wneuper@59553:   # Oct.13: replaced "axioms" by "axiomatization"
wneuper@59553:   # Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref
wneuper@59553:   # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
wneuper@59553:     simplification of multivariate rationals (without improving the rulesets involved).
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>Run tests\<close>
wneuper@59553: text \<open>
wneuper@59553:   Is standard now; this subsection will be discontinued under Isabelle2013-1
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>State of tests\<close>
wneuper@59553: text \<open>
wneuper@59553:   See points in subsection "isac on Isabelle2011", "State of tests".
wneuper@59553:   # re-activated listC.sml
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>Changesets of begin and end\<close>
wneuper@59553: text \<open>
wneuper@59553:   changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"
wneuper@59553:   User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
wneuper@59553:   Date: Tue Nov 19 22:23:30 2013 +0000
wneuper@59553:   :
wneuper@59553:   : isac on Isablle2013 
wneuper@59553:   :
wneuper@59553:   Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
wneuper@59553:   User: Walther Neuper <neuper@ist.tugraz.at>
wneuper@59553:   Date: 2013-07-15 08:28:50 +0200 (4 weeks)
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: subsection \<open>isac on Isabelle2012\<close>
wneuper@59553: subsubsection \<open>Summary of development\<close>
wneuper@59553: text \<open>
wneuper@59553:   isac on Isabelle2012 is considered just a transitional stage
wneuper@59553:   within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
wneuper@59553:   For considerations on the transition see 
wneuper@59553:   ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>Run tests\<close>
wneuper@59553: text \<open>
wneuper@59553: $ cd /usr/local/isabisac12/
wneuper@59553: $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
wneuper@59553: $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>State of tests\<close>
wneuper@59553: text \<open>
wneuper@59553:   At least the tests from isac on Isabelle2011 run again.
wneuper@59553:   However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling 
wneuper@59553:   in parallel with evaluation.
wneuper@59553: 
wneuper@59553:   Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
wneuper@59553:   yields 69 hits, some of which were already present before Isabelle2002-->2009-2
wneuper@59553:   (i.e. on the old notebook from 2002).
wneuper@59553: 
wneuper@59553:   Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
wneuper@59553:   # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
wneuper@59553:   # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
wneuper@59553:   # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
wneuper@59553:   Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
wneuper@59553: 
wneuper@59553:   Some tests have been re-activated (e.g. error patterns, fill patterns).
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>Changesets of begin and end\<close>
wneuper@59553: text \<open>
wneuper@59553:   Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
wneuper@59553:   User: Walther Neuper <neuper@ist.tugraz.at>
wneuper@59553:   Date: 2013-07-11 16:58:31 +0200 (4 weeks)
wneuper@59553:   :
wneuper@59553:   : isac on Isablle2012 
wneuper@59553:   :
wneuper@59553:   Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
wneuper@59553:   User: Walther Neuper <neuper@ist.tugraz.at>
wneuper@59553:   Date: 2012-09-24 18:35:13 +0200 (8 months)
wneuper@59553:   ------------------------------------------------------------------------------
wneuper@59553:   Changeset: 48756 (7443906996a8) merged
wneuper@59553:   User: Walther Neuper <neuper@ist.tugraz.at>
wneuper@59553:   Date: 2012-09-24 18:15:49 +0200 (8 months)
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: subsection \<open>isac on Isabelle2011\<close>
wneuper@59553: subsubsection \<open>Summary of development\<close>
wneuper@59553: text \<open>
wneuper@59553:   isac's mathematics engine has been extended by two developments:
wneuper@59553:   (1) Isabelle's contexts were introduced by Mathias Lehnfeld
wneuper@59553:   (2) Z_Transform was introduced by Jan Rocnik, which revealed
wneuper@59553:     further errors introduced by (1).
wneuper@59553:   (3) "error patterns" were introduced by Gabriella Daroczy
wneuper@59553:   Regressions tests have been added for all of these.
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>Run tests\<close>
wneuper@59553: text \<open>
wneuper@59553:   $ cd /usr/local/isabisac11/
wneuper@59553:   $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
wneuper@59553:   $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>State of tests\<close>
wneuper@59553: text \<open>
wneuper@59553:   Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*) 
wneuper@59553:   and sometimes give reasons for failing tests.
wneuper@59553:   (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable
wneuper@59553:   work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
wneuper@59553: 
wneuper@59553:   The most signification tests (in particular Frontend/interface.sml) run,
wneuper@59553:   however, many "error in kernel" are not caught by an exception.
wneuper@59553:   ------------------------------------------------------------------------------
wneuper@59553:   After the changeset below Test_Isac worked with check_unsynchronized_ref ():
wneuper@59553:   ------------------------------------------------------------------------------
wneuper@59553:   Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
wneuper@59553:   User: Walther Neuper <neuper@ist.tugraz.at>
wneuper@59553:   Date: 2012-08-06 10:38:11 +0200 (11 months)
wneuper@59553: 
wneuper@59553: 
wneuper@59553:   The list below records TODOs while producing an ISAC kernel for 
wneuper@59553:   gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
wneuper@59553:   (so to be resumed with Isabelle2013-1):
wneuper@59553:   ############## WNxxxxxx.TODO can be found in sources ##############
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN111013.TODO: lots of cleanup/removal in test/../Test.thy
wneuper@59553:   --------------------------------------------------------------------------------
walther@59845:   WN111013.TODO: remove concept around "fun implicit_take", lots of troubles with 
wneuper@59553:   this special case (see) --- why not nxt = Model_Problem here ? ---
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
wneuper@59553:   ... FIRST redesign 
wneuper@59553:   # simplify_* , *_simp_* 
wneuper@59553:   # norm_* 
wneuper@59553:   # calc_* , calculate_*  ... require iteration over all rls ...
wneuper@59553:   ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN120314 changeset a393bb9f5e9f drops root equations.
wneuper@59553:   see test/Tools/isac/Knowledge/rootrateq.sml 
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN120317.TODO changeset 977788dfed26 dropped rateq:
wneuper@59553:   # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
wneuper@59553:   # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:    
wneuper@59553:     investigation Check_elementwise stopped due to too much effort finding out,
wneuper@59553:     why Check_elementwise worked in 2002 in spite of the error.
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl 
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN120317.TODO found by test --- interSteps for Schalk 299a --- that 
wneuper@59553:     NO test with 'interSteps' is checked properly (with exn on changed behaviour)
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
wneuper@59553:     a newly outcommented test where rewrite_set_ make_polynomial --> NONE
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN120320.TODO check-improve rlsthmsNOTisac:
wneuper@59553:   DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
wneuper@59553:   DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy 
wneuper@59553:   FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
wneuper@59553:   # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN120320.TODO rlsthmsNOTisac: replace twice thms ^
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
wneuper@59553:   --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN120321.TODO rearrange theories:
wneuper@59553:     Knowledge
wneuper@59553:       :
walther@59603:       Prog_Expr.thy
wneuper@59553:       ///Descript.thy --> ProgLang
walther@59603:       Delete.thy   <--- first_Knowledge_thy (*mv to Prog_Expr.thy*)
wneuper@59553:     ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
wneuper@59553:           Interpret.thy are generated (simplifies xml structure for theories)
wneuper@59585:       Program.thy
wneuper@59553:       Tools.thy
wneuper@59553:       ListC.thy    <--- first_Proglang_thy
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
wneuper@59553:       EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"
wneuper@59553:   broken during work on thy-hierarchy
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
wneuper@59553:   test --- the_hier (get_thes ()) (collect_thydata ())---
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
wneuper@59553:   !!add mutual crossreferences to ?fun headline??? where the same has to be done:
wneuper@59553:   !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
wneuper@59553:   --------------------------------------------------------------------------------
walther@59914:   WN120409.TODO replace "op mem" (2002) with Library.member (2011) ... 
wneuper@59553:   ... an exercise interesting for beginners !
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN120411 scanning html representation of newly generated knowledge:
wneuper@59553:   * thy:
wneuper@59553:   ** Theorems: only "Proof of the theorem" (correct!)
wneuper@59553:                and "(c) isac-team (math-autor)"
wneuper@59553:   ** Rulesets: only "Identifier:///"
wneuper@59553:                and "(c) isac-team (math-autor)"
wneuper@59553:   ** IsacKnowledge: link to dependency graph (which needs to be created first)
wneuper@59553:   ** IsacScripts --> ProgramLanguage
wneuper@59553:   *** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen
wneuper@59553:   
wneuper@59553:   * pbl: OK !?!
wneuper@59553:   * met: OK !?!
wneuper@59553:   * exp: 
wneuper@59553:   ** Z-Transform is missing !!!
wneuper@59553:   ** type-constraints !!!
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553:   WN120417: merging xmldata revealed:
wneuper@59553:   ..............NEWLY generated:........................................
wneuper@59553:   <THEOREMDATA>
wneuper@59553:     <GUH> thy_isab_Fun-thm-o_apply </GUH>
wneuper@59553:     <STRINGLIST>
wneuper@59553:       <STRING> Isabelle </STRING>
wneuper@59553:       <STRING> Fun </STRING>
wneuper@59553:       <STRING> Theorems </STRING>
wneuper@59553:       <STRING> o_apply </STRING>
wneuper@59553:     </STRINGLIST>
wneuper@59553:       <MATHML>
wneuper@59553:         <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
wneuper@59553:       </MATHML>  <PROOF>
wneuper@59553:       <EXTREF>
wneuper@59553:         <TEXT> Proof of the theorem </TEXT>
wneuper@59553:         <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
wneuper@59553:       </EXTREF>
wneuper@59553:     </PROOF>
wneuper@59553:     <EXPLANATIONS> </EXPLANATIONS>
wneuper@59553:     <MATHAUTHORS>
wneuper@59553:       <STRING> Isabelle team, TU Munich </STRING>
wneuper@59553:     </MATHAUTHORS>
wneuper@59553:     <COURSEDESIGNS>
wneuper@59553:     </COURSEDESIGNS>
wneuper@59553:   </THEOREMDATA>
wneuper@59553:   ..............OLD FORMAT:.............................................
wneuper@59553:   <THEOREMDATA>
wneuper@59553:     <GUH> thy_isab_Fun-thm-o_apply </GUH>
wneuper@59553:     <STRINGLIST>
wneuper@59553:       <STRING> Isabelle </STRING>
wneuper@59553:       <STRING> Fun </STRING>
wneuper@59553:       <STRING> Theorems </STRING>
wneuper@59553:       <STRING> o_apply </STRING>
wneuper@59553:     </STRINGLIST>
wneuper@59553:     <THEOREM>
wneuper@59553:       <ID> o_apply </ID>
wneuper@59553:       <MATHML>
wneuper@59553:         <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
wneuper@59553:       </MATHML>
wneuper@59553:     </THEOREM>
wneuper@59553:     <PROOF>
wneuper@59553:       <EXTREF>
wneuper@59553:         <TEXT> Proof of the theorem </TEXT>
wneuper@59553:         <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
wneuper@59553:       </EXTREF>
wneuper@59553:     </PROOF>
wneuper@59553:     <EXPLANATIONS> </EXPLANATIONS>
wneuper@59553:     <MATHAUTHORS>
wneuper@59553:       <STRING> Isabelle team, TU Munich </STRING>
wneuper@59553:     </MATHAUTHORS>
wneuper@59553:     <COURSEDESIGNS>
wneuper@59553:     </COURSEDESIGNS>
wneuper@59553:   </THEOREMDATA>
wneuper@59553:   --------------------------------------------------------------------------------
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>Changesets of begin and end\<close>
wneuper@59553: text \<open>
wneuper@59553:   isac development was done between these changesets:
wneuper@59553:   ------------------------------------------------------------------------------
wneuper@59553:   Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
wneuper@59553:   User: Walther Neuper <neuper@ist.tugraz.at>
wneuper@59553:   Date: 2012-09-24 16:39:30 +0200 (8 months)
wneuper@59553:   :
wneuper@59553:   : isac on Isablle2011
wneuper@59553:   :
wneuper@59553:   Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
wneuper@59553:   Branch: decompose-isar 
wneuper@59553:   User: Walther Neuper <neuper@ist.tugraz.at>
wneuper@59553:   Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
wneuper@59553:   ------------------------------------------------------------------------------
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: subsection \<open>isac on Isabelle2009-2\<close>
wneuper@59553: subsubsection \<open>Summary of development\<close>
wneuper@59553: text \<open>
wneuper@59553:   In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
wneuper@59553:   The update was painful (bridging 7 years of Isabelle development) and cut short 
wneuper@59553:   due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
wneuper@59553:   going on to Isabelle2011 although most of the tests did not run.
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>Run tests\<close>
wneuper@59553: text \<open>
wneuper@59553:   WN131021 this is broken by installation of Isabelle2011/12/13,
wneuper@59553:   because all these write their binaries to ~/.isabelle/heaps/..
wneuper@59553: 
wneuper@59553:   $ cd /usr/local/isabisac09-2/
wneuper@59553:   $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
wneuper@59553:   $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
wneuper@59553:   NOT THE RIGHT VERSION.....    test/Tools/isac/Test_Isac.thy !!!
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>State of tests\<close>
wneuper@59553: text \<open>
wneuper@59553:   Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>Changesets of begin and end\<close>
wneuper@59553: text \<open>
wneuper@59553:   isac development was done between these changesets:
wneuper@59553:   ------------------------------------------------------------------------------
wneuper@59553:   Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
wneuper@59553:   Branch: decompose-isar 
wneuper@59553:   User: Marco Steger <m.steger@student.tugraz.at>
wneuper@59553:   Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
wneuper@59553:   :
wneuper@59553:   : isac on Isablle2009-2
wneuper@59553:   :
wneuper@59553:   Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
wneuper@59553:   Branch: isac-from-Isabelle2009-2 
wneuper@59553:   User: Walther Neuper <neuper@ist.tugraz.at>
wneuper@59553:   Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
wneuper@59553:   ------------------------------------------------------------------------------
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: subsection \<open>isac on Isabelle2002\<close>
wneuper@59553: subsubsection \<open>Summary of development\<close>
wneuper@59553: text \<open>
wneuper@59553:   From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
wneuper@59553:   of isac's mathematics engine has been implemented.
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>Run tests\<close>
wneuper@59553: subsubsection \<open>State of tests\<close>
wneuper@59553: text \<open>
wneuper@59553:   All tests work on an old notebook (the right PolyML coudn't be upgraded to more
wneuper@59553:   recent Linux versions)
wneuper@59553: \<close>
wneuper@59553: subsubsection \<open>Changesets of begin and end\<close>
wneuper@59553: text \<open>
wneuper@59553:   Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
wneuper@59553:   see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
wneuper@59553: \<close>
wneuper@59553: 
wneuper@59553: end
wneuper@59553: (*========== inhibit exn 130719 Isabelle2013 ===================================
wneuper@59553: ============ inhibit exn 130719 Isabelle2013 =================================*)
wneuper@59553: 
wneuper@59553: (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
wneuper@59553:   -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
wneuper@59553: 




