1.1 --- a/test/Tools/isac/Test_Isac.thy	Mon Sep 02 15:17:34 2013 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Sep 02 16:16:08 2013 +0200
     1.3 @@ -2,19 +2,19 @@
     1.4     Author: Walther Neuper 101001
     1.5     (c) copyright due to lincense terms.
     1.6  
     1.7 -   isac tests 
     1.8 -     in ~~/test/Tools/isac are structured according 
     1.9 -     to ~~/src/Tools/isac
    1.10 -   Additional tests are in
    1.11 +   Isac's tests are organised parallel to sources: 
    1.12 +     "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
    1.13 +   plus
    1.14       ~~/test/Tools/isac/ADDTESTS
    1.15 -     ~~/test/Tools/isac/Minisubpbl
    1.16 +     ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
    1.17  
    1.18  $ cd /usr/local/isabisac/
    1.19  $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
    1.20  *)
    1.21  
    1.22 -(*ATTENTION: "Knowledge/biegelinie.sml" NEEDS MANUAL INTERVENTION: 
    1.23 -  Tracing paused.  Stop, or continue with next 100, 1000, 10000 messages?*)
    1.24 +(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
    1.25 +(* !!!!! wait a minute until Isac and the theories below are loaded !!!!! *)
    1.26 +(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
    1.27  
    1.28  theory Test_Isac imports Isac
    1.29    "ADDTESTS/Ctxt"
    1.30 @@ -24,7 +24,7 @@
    1.31    "ADDTESTS/course/phst11/T2_Rewriting"
    1.32    "ADDTESTS/course/phst11/T3_MathEngine"
    1.33    "ADDTESTS/file-depend/BuildC_Test"
    1.34 -  "ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
    1.35 +(*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"*)
    1.36    "~~/test/Pure/Isar/Test_Parsers"
    1.37  (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
    1.38    "~~/test/Pure/Isar/Test_Parse_Term"
    1.39 @@ -33,12 +33,6 @@
    1.40    "~~/src/Tools/isac/Knowledge/GCD_Poly"    (*not imported by Isac.thy*)
    1.41    "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)
    1.42  
    1.43 -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
    1.44 -(* !!!!! wait a minute until Isac and the above theories are loaded !!!!! *)
    1.45 -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
    1.46 -(* !!!!! with this changeset evaluation doen't start < 7min; UG is busy ! *)
    1.47 -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
    1.48 -
    1.49  begin
    1.50  section {* test ML Code of isac *}
    1.51    ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
    1.52 @@ -123,7 +117,7 @@
    1.53    ML_file "Knowledge/rootrat.sml"
    1.54    ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
    1.55    ML_file "Knowledge/partial_fractions.sml"
    1.56 -(*ML_file "Knowledge/polyeq.sml"   -----------------works if cut into parts !!!!!!!!!!!*)
    1.57 +  ML_file "Knowledge/polyeq.sml" (*-----------------works if cut into parts !!!!!!!!!!!*)
    1.58  (*ML_file "Knowledge/rlang.sml"     much to clean up, not urgent due to similar tests  *)
    1.59    ML_file "Knowledge/calculus.sml"
    1.60    ML_file "Knowledge/trig.sml"