neuper@41945: (* Title:  All tests on isac; observe outcommented
neuper@41943:    Author: Walther Neuper 101001
neuper@41943:    (c) copyright due to lincense terms.
neuper@41943: 
neuper@41943: $ cd /usr/local/isabisac/test/Tools/isac
neuper@48884: $ /usr/local/isabisac/bin/isabelle jedit -l Isac Test_Isac.thy &
neuper@41943: *)
neuper@41943: 
neuper@48888: theory Test_Isac imports Isac
neuper@41980:   "ADDTESTS/Ctxt"
neuper@42048:   "ADDTESTS/test-depend/Build_Test"
neuper@42023:   "ADDTESTS/All_Ctxt"
neuper@42179:   "ADDTESTS/course/phst11/T1_Basics"
neuper@42092:   "ADDTESTS/course/phst11/T2_Rewriting"
neuper@42179:   "ADDTESTS/course/phst11/T3_MathEngine"
neuper@42048:   "ADDTESTS/file-depend/Build_Test"
neuper@42280:   "ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
neuper@42048:   "../../Pure/Isar/Test_Parsers"
neuper@42048: (*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)
neuper@42048:   "../../Pure/Isar/Test_Parse_Term"
neuper@42387: 
neuper@41945: uses 
neuper@41945:   (         "library.sml")
neuper@41945:   (         "calcelems.sml")
neuper@42185:   ("ProgLang/termC.sml")      
neuper@41945:   ("ProgLang/calculate.sml")
neuper@41945:   ("ProgLang/rewrite.sml")
neuper@48895:   (*"ProgLang/listC.sml"*)
akargl@42176:   ("ProgLang/scrtools.sml")
akargl@42176:   ("ProgLang/tools.sml")
neuper@41945: 
neuper@41985:   ("Minisubpbl/000-comments.sml")
neuper@41985:   ("Minisubpbl/100-init-rootpbl.sml")
neuper@41986:   ("Minisubpbl/150-add-given.sml")
neuper@41985:   ("Minisubpbl/200-start-method.sml")
neuper@41985:   ("Minisubpbl/300-init-subpbl.sml")
neuper@41985:   ("Minisubpbl/400-start-meth-subpbl.sml")
neuper@42022:   ("Minisubpbl/490-nxt-Check_Postcond.sml")
neuper@42022:   ("Minisubpbl/500-met-sub-to-root.sml")
neuper@42022:   ("Minisubpbl/530-error-Check_Elementwise.sml")
neuper@42022:   ("Minisubpbl/600-postcond.sml")
neuper@41985: 
neuper@41945:   ("Interpret/mstools.sml") 
bonzai@41951:   ("Interpret/ctree.sml")
neuper@41945:   ("Interpret/ptyps.sml") 
akargl@42176:   ("Interpret/generate.sml")
neuper@41945:   ("Interpret/calchead.sml") 
akargl@42176:   ("Interpret/appl.sml")
neuper@41945:   ("Interpret/rewtools.sml") 
akargl@42169:   ("Interpret/script.sml")
akargl@42176:   ("Interpret/solve.sml") 
akargl@42176:   ("Interpret/inform.sml")
neuper@41945:   ("Interpret/mathengine.sml")
neuper@41945: 
akargl@42176:   ("xmlsrc/mathml.sml")
neuper@41945:   ("xmlsrc/datatypes.sml")
neuper@41945:   ("xmlsrc/pbl-met-hierarchy.sml")
neuper@48895:   (*"xmlsrc/thy-hierarchy.sml"*)
neuper@41945:   ("xmlsrc/interface-xml.sml")
neuper@41945: 
neuper@41945:   ("Frontend/messages.sml")
neuper@41945:   ("Frontend/states.sml")
neuper@41945:   ("Frontend/interface.sml")
neuper@41945:   ("print_exn_G.sml")
neuper@41945: 
neuper@41945:   ("Knowledge/delete.sml")
neuper@41945:   ("Knowledge/descript.sml")
neuper@41945:   ("Knowledge/atools.sml")
neuper@41945:   ("Knowledge/simplify.sml")
neuper@41945:   ("Knowledge/poly.sml")
neuper@48884: (*THIS WAITS UNTIL Isabelle2013: ("Knowledge/gcd_poly.sml") ("Knowledge/gcd_poly_winkler.sml")
neuper@48884:   IN THIS SEQUENCE: SEE Test_Some2.thy*)
neuper@48895:   (*"Knowledge/rational.sml"*)
neuper@41945:   ("Knowledge/equation.sml")
neuper@41945:   ("Knowledge/root.sml")
neuper@41945:   ("Knowledge/lineq.sml")
neuper@48895:   (*"Knowledge/rooteq.sml"*)
neuper@41945:   ("Knowledge/rateq.sml")
neuper@41945:   ("Knowledge/rootrateq.sml")
neuper@42185:   ("Knowledge/polyeq.sml")
neuper@41945:   ("Knowledge/calculus.sml")
neuper@41945:   ("Knowledge/trig.sml")
neuper@48895:   (*"Knowledge/logexp.sml"*)
neuper@41945:   ("Knowledge/diff.sml")
neuper@41945:   ("Knowledge/integrate.sml")
neuper@41945:   ("Knowledge/eqsystem.sml")
neuper@41945:   ("Knowledge/test.sml")
neuper@42289:   ("Knowledge/partial_fractions.sml")
neuper@41945:   ("Knowledge/polyminus.sml")
neuper@41945:   ("Knowledge/vect.sml")
neuper@41945:   ("Knowledge/diffapp.sml")
neuper@41945:   ("Knowledge/biegelinie.sml")
neuper@41945:   ("Knowledge/algein.sml")
neuper@41945:   ("Knowledge/diophanteq.sml")
neuper@42412:   ("Knowledge/Inverse_Z_Transform/inverse_z_transform.sml")
neuper@41945:   ("Knowledge/isac.sml")
neuper@42407:   ("Knowledge/build_thydata.sml")
neuper@41945: 
neuper@41943: begin
neuper@48895: section {* test ML Code of isac *}
neuper@48895:   ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
neuper@42179:   use          "library.sml"
neuper@42179:   use          "calcelems.sml"
akargl@42188:   use "ProgLang/termC.sml"
t@42225:   use "ProgLang/calculate.sml"
t@42227:   use "ProgLang/rewrite.sml"
neuper@42185: (*use "ProgLang/listC.sml"            2002*)
t@42225:   use "ProgLang/scrtools.sml"
t@42225:   use "ProgLang/tools.sml"
neuper@41943:   ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
neuper@41986:   ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
neuper@41985:   use "Minisubpbl/000-comments.sml"
neuper@41985:   use "Minisubpbl/100-init-rootpbl.sml"
neuper@41986:   use "Minisubpbl/150-add-given.sml"
neuper@41985:   use "Minisubpbl/200-start-method.sml"
neuper@41990:   use "Minisubpbl/300-init-subpbl.sml"
neuper@41997:   use "Minisubpbl/400-start-meth-subpbl.sml"
neuper@42022:   use "Minisubpbl/490-nxt-Check_Postcond.sml"
neuper@41998:   use "Minisubpbl/500-met-sub-to-root.sml"
neuper@42022:   use "Minisubpbl/530-error-Check_Elementwise.sml"
neuper@41998:   use "Minisubpbl/600-postcond.sml"
akargl@42188:   ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
neuper@41943:   ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
neuper@42185:   use "Interpret/mstools.sml"
neuper@41989:   use "Interpret/ctree.sml"         (*!...!see(25)*)
neuper@42390:   use "Interpret/ptyps.sml"
neuper@48891:   ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}
neuper@48895: (*TRICK DOESN'T WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)
neuper@42321:   use "Interpret/generate.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*)
neuper@48895:   use "Interpret/calchead.sml"
neuper@48894:   use "Interpret/appl.sml"          (*complete "WEGEN INTERMED TESTCODE"                          *)
neuper@48894:   use "Interpret/rewtools.sml"      (*complete, isac's Context broken at 2009-2 --> 2011, thehier!*)
neuper@48895:   use "Interpret/script.sml"
neuper@48895:   use "Interpret/solve.sml"
neuper@48895:   use "Interpret/inform.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*)
neuper@41972:   use "Interpret/mathengine.sml"    (*!part.*)
neuper@41943:   ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
neuper@41943:   ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
neuper@48895:   use "xmlsrc/mathml.sml"           (*part.*)
neuper@48895:   use "xmlsrc/datatypes.sml"        (*TODO/part.*)
neuper@48895:   use "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
neuper@48895: (*use "xmlsrc/thy-hierarchy.sml"      TODO after 2009-2/part | Isabelle2012-->13 !thehier! *)
neuper@48895: (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
neuper@48895: val it = "----------- ### thes2file ... Exception- Match raised -----------": string
neuper@48889: :
neuper@48889: val it = "~~~~~ fun thes2file, args:": string
neuper@48889: val p = "../../tmp/": path
neuper@48889: val it = (): unit
neuper@48889:  exception Bind raised (line 359 of "~~/test/Tools/isac/xmlsrc/thy-hierarchy.sml")
neuper@48889:                                                  ...CONCERNED WITH thehier
neuper@48889: *)
akargl@42176:   use "xmlsrc/interface-xml.sml"     (*TODO after 2009-2*)
neuper@41943:   ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
neuper@41943:   ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
neuper@42321:   use "Frontend/messages.sml"
neuper@42321:   use "Frontend/states.sml"
t@42225:   use "Frontend/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*)
neuper@42407:   use          "print_exn_G.sml"
neuper@41943:   ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
neuper@48895:   ML {*"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";*}
neuper@42321:   use "Knowledge/delete.sml"
neuper@42321:   use "Knowledge/descript.sml"
neuper@42397:   use "Knowledge/atools.sml"
neuper@42396:   use "Knowledge/simplify.sml"
neuper@42395:   use "Knowledge/poly.sml"
neuper@48884: (*THIS WAITS UNTIL Isabelle2013 IN THIS SEQUENCE (SEE Test_Some2.thy):0
neuper@48884:   use "Knowledge/gcd_poly.sml" (*type error 'nth' etc*)
neuper@48884:   use "Knowledge/gcd_poly_winkler.sml"*)
neuper@42399: (*use "Knowledge/rational.sml"  WN120317.TODO postponed to joint work with dmeindl *)
neuper@42395:   use "Knowledge/equation.sml"
neuper@42395:   use "Knowledge/root.sml"
neuper@42395:   use "Knowledge/lineq.sml"
neuper@42395: (*use "Knowledge/rooteq.sml"    some complicated equations not recovered from 2002 *)
neuper@42395:   use "Knowledge/rateq.sml"   (*some complicated equations not recovered from 2002 *)
neuper@42392:   use "Knowledge/rootrat.sml"
neuper@42397:   use "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
neuper@42289:   use "Knowledge/partial_fractions.sml"
neuper@42319:   use "Knowledge/polyeq.sml"
neuper@42413: (*use "Knowledge/rlang.sml"     much to clean up, not urgent due to similar tests  *)
neuper@42321:   use "Knowledge/calculus.sml"
t@42225:   use "Knowledge/trig.sml"
neuper@42393: (*use "Knowledge/logexp.sml"    not included as stuff for presentation of authoring*) 
neuper@42393:   use "Knowledge/diff.sml"
neuper@42393:   use "Knowledge/integrate.sml"
neuper@42391:   use "Knowledge/eqsystem.sml"
t@42225:   use "Knowledge/test.sml"
neuper@42390:   use "Knowledge/polyminus.sml"
t@42225:   use "Knowledge/vect.sml"
neuper@42399:   use "Knowledge/diffapp.sml"        (* postponed to dev. specification | TP-prog. *)
neuper@42387:   use "Knowledge/biegelinie.sml"
neuper@42385:   use "Knowledge/algein.sml"
t@42225:   use "Knowledge/diophanteq.sml"
neuper@42412:   use "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
neuper@42399:   use "Knowledge/isac.sml"
neuper@42400:   use "Knowledge/build_thydata.sml"
neuper@48895:   ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}
neuper@41945:   ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
neuper@41945:   ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
neuper@41945:   ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
neuper@41943: 
neuper@48895: section {* history of tests *}
neuper@48895: text {*
neuper@48895:   Systematic regression tests have been introduced to isac development in 2003.
neuper@48895:   Sanity of the regression test suffered 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. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
neuper@48895: *}
neuper@48895: 
neuper@48895: subsection {* isac on Isabelle2013 *}
neuper@48895: subsubsection {* Summary of development *}
neuper@48895: text {*
neuper@48895: *}
neuper@48895: subsubsection {* Run tests *}
neuper@48895: text {*
neuper@48895: *}
neuper@48895: subsubsection {* State of tests *}
neuper@48895: text {*
neuper@48895: *}
neuper@48895: subsubsection {* Changesets of begin and end *}
neuper@48895: text {*
neuper@48895: *}
neuper@48895: 
neuper@48895: subsection {* isac on Isabelle2012 *}
neuper@48895: subsubsection {* Summary of development *}
neuper@48895: text {*
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..".
neuper@48895: *}
neuper@48895: subsubsection {* Run tests *}
neuper@48895: text {*
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
neuper@48895: *}
neuper@48895: subsubsection {* State of tests *}
neuper@48895: text {*
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).
neuper@48895: *}
neuper@48895: subsubsection {* Changesets of begin and end *}
neuper@48895: text {*
neuper@48895:   TODO
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)
neuper@48895: *}
neuper@48895: 
neuper@48895: subsection {* isac on Isabelle2011 *}
neuper@48895: subsubsection {* Summary of development *}
neuper@48895: text {*
neuper@48895:   isac's mathematics engine has been extended by two developments:
neuper@48895:   (1) Isabelle's contexts were introduced by Mathias Lehnfeld
neuper@48895:   (2) "error patterns" were introduced by Gabriella Daroczy
neuper@48895:   Regressions tests have been added for both.
neuper@48895: *}
neuper@48895: subsubsection {* Run tests *}
neuper@48895: text {*
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
neuper@48895: *}
neuper@48895: subsubsection {* State of tests *}
neuper@48895: text {* 
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:   Tests with functions decomposed for single-stepping are marked with
neuper@48895:   "~~~~~ fun , args:"; val 
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@48895: *}
neuper@48895: subsubsection {* Changesets of begin and end *}
neuper@48895: text {*
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:   ------------------------------------------------------------------------------
neuper@48895: *}
neuper@48895: 
neuper@48895: subsection {* isac on Isabelle2009-2 *}
neuper@48895: subsubsection {* Summary of development *}
neuper@48895: text {*
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.
neuper@48895: *}
neuper@48895: subsubsection {* Run tests *}
neuper@48895: text {*
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 !!!
neuper@48895: *}
neuper@48895: subsubsection {* State of tests *}
neuper@48895: text {* 
neuper@48895:   Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
neuper@48895:   If really necessary, go back to the old notebook with Isabelle2002.
neuper@48895: *}
neuper@48895: subsubsection {* Changesets of begin and end *}
neuper@48895: text {*
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:   ------------------------------------------------------------------------------
neuper@48895: *}
neuper@48895: 
neuper@48895: subsection {* isac on Isabelle2002 *}
neuper@48895: subsubsection {* Summary of development *}
neuper@48895: text {*
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.
neuper@48895: *}
neuper@48895: subsubsection {* Run tests *}
neuper@48895: subsubsection {* State of tests *}
neuper@48895: text {* 
neuper@48895:   All tests work on an old notebook (the right PolyML coudn't be upgraded to more
neuper@48895:   recent Linux versions)
neuper@48895: *}
neuper@48895: subsubsection {* Changesets of begin and end *}
neuper@48895: text {*
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.
neuper@48895: *}
neuper@48895: 
neuper@41943: end
neuper@42067: (*========== inhibit exn 110628 ================================================
neuper@42067: ============ inhibit exn 110628 ==============================================*)
neuper@41943: 
neuper@41943: (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
neuper@48895: Pending source file dependencies: "Knowledge/algein.sml" 
neuper@48895:   -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
neuper@41975: