| branch | isac-update-Isa09-2 |
| changeset 37965 | 9c11005c33b8 |
| parent 37949 | aaf528d3ebd5 |
| child 48762 | 3a8f672472a8 |
| 37964:f72dd3f427e4 | 37965:9c11005c33b8 |
|---|---|
1 theory Foo_Know111 imports "../1language/Foo_Language" begin |
1 theory Foo_Know111 imports "../1language/Foo_Language" Complex_Main begin |
2 |
2 |
3 consts foo111 :: "'a" |
3 consts foo111 :: "'a" |
4 bar111 :: "'a" |
4 bar111 :: "'a" |
5 axioms code111 : "foo111 = bar111" |
5 axioms code111 : "foo111 = bar111" |
6 |
6 |
7 ML {* |
7 ML {* |
8 (* there is an error when de-commenting *) 111 |
8 @{thm code111}; |
9 *} |
9 *} |
10 |
10 |
11 end |
11 end |