1.1 --- a/test/Tools/isac/Test_Isac.thy	Sun Jun 16 12:31:41 2013 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Sun Jun 16 13:10:32 2013 +0200
     1.3 @@ -9,9 +9,18 @@
     1.4  *)
     1.5  
     1.6  theory Test_Isac imports
     1.7 -  Isac
     1.8 -  "Knowledge/Rational_Test"
     1.9 +(*Isac
    1.10 +OUTCOMMENT THE ABOVE AND SET <Prover Session> <Isac> (INSTEAD OF 'HOL') 
    1.11 +
    1.12 +<Isac> HAS BEEN CREATED BY /usr/local/isabisac/bin/isabelle usedir -b HOL Isac,
    1.13 +CREATION SEEMS TO BE CORRECT:
    1.14 +$ ls -l  "/home/neuper/.isabelle/Isabelle2012/heaps/polyml-5.4.1_x86_64-linux/Isac"
    1.15 +-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.16 +*)
    1.17 +(*"Knowledge/Rational_Test" ...THIS FILE HAS DISAPPEARED*)
    1.18    "ADDTESTS/Ctxt"
    1.19 +(*CAUSES ERROR: Bad theory (file "/usr/local/isabisac/test/Tools/isac/ADDTESTS/All_Ctxt.thy") 
    1.20 +??? HOW CAN I MAKE <Prover Session> <Isac> WORK FOR Test_Isac.thy ??? *)
    1.21    "ADDTESTS/test-depend/Build_Test"
    1.22    "ADDTESTS/All_Ctxt"
    1.23    "ADDTESTS/course/phst11/T1_Basics"