2 |
2 |
3 use "0foolibrary.ML" |
3 use "0foolibrary.ML" |
4 use_thy "1language/Foo_Language" |
4 use_thy "1language/Foo_Language" |
5 use "2interpreter/2foointerpreter.ML" |
5 use "2interpreter/2foointerpreter.ML" |
6 |
6 |
|
7 (*vvvvvvv can be bypassed with Foo_KnowALL |
7 use_thy "3knowledge/Foo_Know111" |
8 use_thy "3knowledge/Foo_Know111" |
8 use_thy "3knowledge/Foo_Know222" |
9 use_thy "3knowledge/Foo_Know222" |
|
10 ^^^^^^^ can be bypassed with Foo_KnowALL*) |
|
11 use_thy "3knowledge/Foo_KnowALL" |
9 |
12 |
10 |
13 text {* the different theories of knowledge are recognized, Const bar*: *} |
11 ML {* (* the different theories of knowledge are recognized, Const: *) |
14 ML {* |
12 |
|
13 val trm = Syntax.read_term_global @{theory Foo_Know111} |
15 val trm = Syntax.read_term_global @{theory Foo_Know111} |
14 "fooprog (foo111 = bar111)"; |
16 "fooprog (foo111 = bar111)"; |
15 foointerpret trm; |
17 val Const ("Foo_Know111.bar111", _) = foointerpret trm; |
16 (*Const ("Foo_Know111.bar111", "'a") : term*) |
|
17 |
18 |
18 val trm = Syntax.read_term_global @{theory Foo_Know222} |
19 val trm = Syntax.read_term_global @{theory Foo_Know222} |
19 "fooprog (foo222 = bar222)"; |
20 "fooprog (foo222 = bar222)"; |
20 foointerpret trm; |
21 val Const ("Foo_Know222.bar222", _) = foointerpret trm; |
21 (*val it = Const ("Foo_Know222.bar222", "'a") : term*) |
|
22 *} |
22 *} |
23 |
23 |
24 ML {* (* the different theories of knowledge are recognized, Free: *) |
24 text {* the different theories of knowledge are recognized, Free bar*: *} |
|
25 ML {* |
25 val trm = Syntax.read_term_global @{theory Foo_Know111} |
26 val trm = Syntax.read_term_global @{theory Foo_Know111} |
26 "fooprog (foo222 = bar222)"; |
27 "fooprog (foo222 = bar222)"; |
27 (*Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $ |
28 (*Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $ |
28 (Const ("op =", "'a => 'a => bool") $ Free ("foo222", "'a") $ |
29 (Const ("op =", "'a => 'a => bool") $ Free ("foo222", "'a") $ |
29 Free ("bar222", "'a")) |
30 Free ("bar222", "'a")) |