test/Tools/isac/ADDTESTS/file-depend/3knowledge/Foo_Know111.thy
branchisac-update-Isa09-2
changeset 37965 9c11005c33b8
parent 37949 aaf528d3ebd5
child 48762 3a8f672472a8
     1.1 --- a/test/Tools/isac/ADDTESTS/file-depend/3knowledge/Foo_Know111.thy	Tue Aug 31 11:10:30 2010 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/3knowledge/Foo_Know111.thy	Tue Aug 31 15:36:57 2010 +0200
     1.3 @@ -1,11 +1,11 @@
     1.4 -theory Foo_Know111 imports "../1language/Foo_Language" begin
     1.5 +theory Foo_Know111 imports "../1language/Foo_Language" Complex_Main begin
     1.6  
     1.7  consts foo111 :: "'a"
     1.8         bar111 :: "'a"
     1.9  axioms code111 : "foo111 = bar111"
    1.10  
    1.11  ML {*
    1.12 -(* there is an error when de-commenting *) 111
    1.13 +@{thm code111};
    1.14  *}
    1.15  
    1.16  end
    1.17 \ No newline at end of file