equal
deleted
inserted
replaced
28 precompiled versions of the given datatypes and functions. This |
28 precompiled versions of the given datatypes and functions. This |
29 also allows to refer to the referenced datatypes and functions from |
29 also allows to refer to the referenced datatypes and functions from |
30 arbitrary ML code as well. |
30 arbitrary ML code as well. |
31 |
31 |
32 A typical example for @{command code_reflect} can be found in the |
32 A typical example for @{command code_reflect} can be found in the |
33 @{theory Predicate} theory. |
33 @{theory HOL.Predicate} theory. |
34 \<close> |
34 \<close> |
35 |
35 |
36 |
36 |
37 subsubsection \<open>Separate compilation\<close> |
37 subsubsection \<open>Separate compilation\<close> |
38 |
38 |