equal
deleted
inserted
replaced
2 Author: Andreas Lochbihler |
2 Author: Andreas Lochbihler |
3 *) |
3 *) |
4 |
4 |
5 header {* A generic phantom type *} |
5 header {* A generic phantom type *} |
6 |
6 |
7 theory Phantom_Type imports "~~/src/HOL/Main" begin |
7 theory Phantom_Type imports Main begin |
8 |
8 |
9 datatype ('a, 'b) phantom = phantom 'b |
9 datatype ('a, 'b) phantom = phantom 'b |
10 |
10 |
11 primrec of_phantom :: "('a, 'b) phantom \<Rightarrow> 'b" |
11 primrec of_phantom :: "('a, 'b) phantom \<Rightarrow> 'b" |
12 where "of_phantom (phantom x) = x" |
12 where "of_phantom (phantom x) = x" |