| author | Walther Neuper <neuper@ist.tugraz.at> |
| Sat, 26 Feb 2011 12:37:58 +0100 | |
| branch | decompose-isar |
| changeset 41900 | 8391d3789efb |
| parent 41899 | d837e83a4835 |
| child 48762 | 3a8f672472a8 |
| permissions | -rw-r--r-- |
| neuper@41900 | 1 |
(*theory Foo_Language imports Build_Test*) |
| neuper@41899 | 2 |
theory Foo_Language imports Complex_Main |
| neuper@41899 | 3 |
uses ("../0foolibrary.ML")
|
| neuper@37946 | 4 |
begin |
| neuper@41899 | 5 |
use "../0foolibrary.ML" |
| neuper@37946 | 6 |
|
| neuper@37946 | 7 |
typedecl foosource |
| neuper@37946 | 8 |
consts fooprog :: "'a => foosource" |
| neuper@37946 | 9 |
|
| neuper@37946 | 10 |
ML {* (* the library function is recognized *)
|
| neuper@41899 | 11 |
foolibrhs @{term "a = b"}
|
| neuper@37946 | 12 |
*} |
| neuper@41899 | 13 |
ML {* tracing (PolyML.makestring @{theory}); *}
|
| neuper@37946 | 14 |
end |