1.1 --- a/test/Tools/isac/Test_Isac.thy	Tue Jun 18 08:19:57 2013 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Tue Jun 18 17:51:36 2013 +0200
     1.3 @@ -3,28 +3,17 @@
     1.4     (c) copyright due to lincense terms.
     1.5  
     1.6  $ cd /usr/local/isabisac/test/Tools/isac
     1.7 -$ /usr/local/Isabelle/bin/isabelle jedit -l Isac Test_Isac.thy &
     1.8 -1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
     1.9 -        10        20        30        40        50        60        70        80         90      100
    1.10 +$ /usr/local/isabisac/bin/isabelle jedit -l Isac Test_Isac.thy &
    1.11  *)
    1.12  
    1.13  theory Test_Isac imports
    1.14 +  "~~/src/Tools/isac/Frontend/Isac"
    1.15  (*Isac
    1.16 -OUTCOMMENT THE ABOVE AND SET <Prover Session> <Isac> (INSTEAD OF 'HOL') 
    1.17 -
    1.18 -<Isac> HAS BEEN CREATED BY /usr/local/isabisac/bin/isabelle usedir -b HOL Isac,
    1.19 -CREATION SEEMS TO BE CORRECT:
    1.20 -$ ls -l  "/home/neuper/.isabelle/Isabelle2012/heaps/polyml-5.4.1_x86_64-linux/Isac"
    1.21 --r--r--r-- 1 neuper neuper 296349832 Jun 16 11:41 /home/neuper/.isabelle/Isabelle2012/heaps/polyml-5.4.1_x86_64-linux/Isac
    1.22 -*)
    1.23 +OUTCOMMENT THE ABOVE AND SET <Prover Session> <Isac> (INSTEAD OF 'HOL')*)
    1.24  (*"Knowledge/Rational_Test" ...THIS FILE HAS DISAPPEARED*)
    1.25    "ADDTESTS/Ctxt"
    1.26    "ADDTESTS/test-depend/Build_Test"
    1.27    "ADDTESTS/All_Ctxt"
    1.28 -(*CAUSES ERROR: Bad theory (file "/usr/local/isabisac/test/Tools/isac/ADDTESTS/All_Ctxt.thy")
    1.29 -
    1.30 -THIS IS THE FIRST FILE WHICH (MORE OR LESS) REQUIRES imports isac.
    1.31 -??? HOW CAN I MAKE <Prover Session> <Isac> WORK FOR Test_Isac.thy ??? *)
    1.32    "ADDTESTS/course/phst11/T1_Basics"
    1.33    "ADDTESTS/course/phst11/T2_Rewriting"
    1.34    "ADDTESTS/course/phst11/T3_MathEngine"
    1.35 @@ -40,7 +29,7 @@
    1.36    ("ProgLang/termC.sml")      
    1.37    ("ProgLang/calculate.sml")
    1.38    ("ProgLang/rewrite.sml")
    1.39 -  ("ProgLang/listg.sml")
    1.40 +  ("ProgLang/listC.sml")
    1.41    ("ProgLang/scrtools.sml")
    1.42    ("ProgLang/tools.sml")
    1.43  
    1.44 @@ -83,6 +72,8 @@
    1.45    ("Knowledge/atools.sml")
    1.46    ("Knowledge/simplify.sml")
    1.47    ("Knowledge/poly.sml")
    1.48 +(*THIS WAITS UNTIL Isabelle2013: ("Knowledge/gcd_poly.sml") ("Knowledge/gcd_poly_winkler.sml")
    1.49 +  IN THIS SEQUENCE: SEE Test_Some2.thy*)
    1.50    ("Knowledge/rational.sml")
    1.51    ("Knowledge/equation.sml")
    1.52    ("Knowledge/root.sml")
    1.53 @@ -166,6 +157,10 @@
    1.54    use "Knowledge/atools.sml"
    1.55    use "Knowledge/simplify.sml"
    1.56    use "Knowledge/poly.sml"
    1.57 +(*THIS WAITS UNTIL Isabelle2013 IN THIS SEQUENCE (SEE Test_Some2.thy):0
    1.58 +  use "Knowledge/gcd_poly.sml" (*type error 'nth' etc*)
    1.59 +  use "Knowledge/gcd_poly_winkler.sml"*)
    1.60 +  use "Knowledge/gcd_poly.sml"
    1.61    use "Knowledge/gcd_poly_winkler.sml"
    1.62  (*use "Knowledge/rational.sml"  WN120317.TODO postponed to joint work with dmeindl *)
    1.63    use "Knowledge/equation.sml"