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




