| author | Walther Neuper <wneuper@ist.tugraz.at> |
| Fri, 22 Jan 2016 15:53:13 +0100 | |
| changeset 59209 | 907ce624bd20 |
| permissions | -rw-r--r-- |
| wneuper@59209 | 1 |
theory HOL_Operations |
| wneuper@59209 | 2 |
imports "../isabelle/2015/Protocol" Main |
| wneuper@59209 | 3 |
begin |
| wneuper@59209 | 4 |
|
| wneuper@59209 | 5 |
operation_setup mk_int = \<open> |
| wneuper@59209 | 6 |
{from_lib = Codec.int,
|
| wneuper@59209 | 7 |
to_lib = Codec.term, |
| wneuper@59209 | 8 |
action = HOLogic.mk_number @{typ int}}\<close>
|
| wneuper@59209 | 9 |
|
| wneuper@59209 | 10 |
operation_setup mk_list = \<open> |
| wneuper@59209 | 11 |
{from_lib = Codec.tuple Codec.typ (Codec.list Codec.term),
|
| wneuper@59209 | 12 |
to_lib = Codec.term, |
| wneuper@59209 | 13 |
action = uncurry HOLogic.mk_list} |
| wneuper@59209 | 14 |
\<close> |
| wneuper@59209 | 15 |
|
| wneuper@59209 | 16 |
end |