| author | Walther Neuper <neuper@ist.tugraz.at> |
| Tue, 01 Mar 2011 15:23:59 +0100 | |
| branch | decompose-isar |
| changeset 41905 | b772eb34c16c |
| parent 41899 | d837e83a4835 |
| child 41922 | 32d7766945fb |
| permissions | -rw-r--r-- |
1 (*2foointerpreter.ML*)
3 fun foointerpret ((Const ("Foo_Language.fooprog", _)) $ (_ $ _ $ res)) = res;
5 (* Foo_Language's definitions are recognized: *)
6 (*val trm = Syntax.read_term_global @{theory Foo_Language} "fooprog (a = b)"; *)
7 val trm = Syntax.read_term_global @{theory "../1language/Foo_Language"}
8 "fooprog (a = b)";
9 (*val trm =
10 Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $
11 (Const ("op =", "'a => 'a => bool") $ Free ("a", "'a") $
12 Free ("b", "'a"))
13 : term*)
14 foointerpret trm;