equal
deleted
inserted
replaced
123 use"diffapp.sml"; |
123 use"diffapp.sml"; |
124 use"biegelinie.sml"; |
124 use"biegelinie.sml"; |
125 use"algein.sml"; |
125 use"algein.sml"; |
126 *) |
126 *) |
127 ML {* |
127 ML {* |
128 theory "Isac" |
128 Thy_Info.get_theory "Isac" |
129 *} |
129 *} |
130 use "../../../test/Tools/isac/Knowledge/isac.sml"; (**) |
130 use "../../../test/Tools/isac/Knowledge/isac.sml"; (**) |
131 |
131 |
132 ML {*print_depth 3*} |
132 ML {*print_depth 3*} |
133 ML {*111*} |
133 ML {*111*} |
137 *) |
137 *) |
138 (* TODO |
138 (* TODO |
139 use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test" |
139 use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test" |
140 : |
140 : |
141 *** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library" |
141 *** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library" |
142 *** Theory loader: the error(s) above occurred while examining theory "Foo_Language" |
142 *** Theory loader: the error(s) above occurred while examining Thy_Info.get_theory "Foo_Language" |
143 |
143 |
144 use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test" |
144 use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test" |
145 *) |
145 *) |
146 use "../../../test/Pure/library.sml" (**) |
146 use "../../../test/Pure/library.sml" (**) |
147 use_thy "../../../test/Pure/General/Basics" |
147 use_thy "../../../test/Pure/General/Basics" |