equal
deleted
inserted
replaced
1 (*2foointerpreter.ML*) |
1 (*2foointerpreter.ML*) |
2 |
2 |
3 fun foointerpret ((Const ("Foo_Language.fooprog", _)) $ (_ $ _ $ res)) = res; |
3 fun foointerpret ((Const ("Foo_Language.fooprog", _)) $ (_ $ _ $ res)) = res; |
4 |
4 |
5 (* Foo_Language's definitions are recognized: *) |
5 (* Foo_Language's definitions are recognized: *) |
6 val trm = Syntax.read_term_global @{theory Foo_Language} "fooprog (a = b)"; |
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)"; |
7 (*val trm = |
9 (*val trm = |
8 Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $ |
10 Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $ |
9 (Const ("op =", "'a => 'a => bool") $ Free ("a", "'a") $ |
11 (Const ("op =", "'a => 'a => bool") $ Free ("a", "'a") $ |
10 Free ("b", "'a")) |
12 Free ("b", "'a")) |
11 : term*) |
13 : term*) |