| author | Walther Neuper <neuper@ist.tugraz.at> |
| Fri, 13 Sep 2013 18:57:11 +0200 | |
| changeset 52102 | cd5494eb08fd |
| child 59472 | 3e904f8ec16c |
| permissions | -rw-r--r-- |
| neuper@52102 | 1 |
theory Foo imports Bar begin |
| neuper@52102 | 2 |
ML {*
|
| neuper@52102 | 3 |
@{theory Bar}; (*OK *)
|
| neuper@52102 | 4 |
(*Thy_Info.get_theory "Bar"; ERROR 'Theory loader: undefined theory entry for "Bar"'*) |
| neuper@52102 | 5 |
case Thy_Info.lookup_theory "Bar" of |
| neuper@52102 | 6 |
NONE => writeln "Expected, if Foo.thy is loaded directly. " |
| neuper@52102 | 7 |
| SOME _ => writeln "Expected, if Foo.thy is loaded within *session* Bar." |
| neuper@52102 | 8 |
*} |
| neuper@52102 | 9 |
end |