Mercurial Mercurial > wneuper > isa / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Test_Isac.thy
changeset 48882 9573e2b07a71
parent 48881 264bb401b7b9
child 48884 b933b88a268a 
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Sun Jun 16 13:10:32 2013 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Sun Jun 16 13:18:10 2013 +0200
     1.3 @@ -19,10 +19,12 @@
     1.4  *)
     1.5  (*"Knowledge/Rational_Test" ...THIS FILE HAS DISAPPEARED*)
     1.6    "ADDTESTS/Ctxt"
     1.7 -(*CAUSES ERROR: Bad theory (file "/usr/local/isabisac/test/Tools/isac/ADDTESTS/All_Ctxt.thy") 
     1.8 -??? HOW CAN I MAKE <Prover Session> <Isac> WORK FOR Test_Isac.thy ??? *)
     1.9    "ADDTESTS/test-depend/Build_Test"
    1.10    "ADDTESTS/All_Ctxt"
    1.11 +(*CAUSES ERROR: Bad theory (file "/usr/local/isabisac/test/Tools/isac/ADDTESTS/All_Ctxt.thy")
    1.12 +
    1.13 +THIS IS THE FIRST FILE WHICH (MORE OR LESS) REQUIRES imports isac.
    1.14 +??? HOW CAN I MAKE <Prover Session> <Isac> WORK FOR Test_Isac.thy ??? *)
    1.15    "ADDTESTS/course/phst11/T1_Basics"
    1.16    "ADDTESTS/course/phst11/T2_Rewriting"
    1.17    "ADDTESTS/course/phst11/T3_MathEngine"
wneuper/isa