src/HOL/Library/Phantom_Type.thy
changeset 58249 180f1b3508ed
parent 52147 9943f8067f11
child 58310 91ea607a34d8
equal deleted inserted replaced
58248:25af24e1f37b 58249:180f1b3508ed
     6 
     6 
     7 theory Phantom_Type
     7 theory Phantom_Type
     8 imports Main
     8 imports Main
     9 begin
     9 begin
    10 
    10 
    11 datatype ('a, 'b) phantom = phantom 'b
    11 datatype_new ('a, 'b) phantom = phantom 'b
    12 
    12 
    13 primrec of_phantom :: "('a, 'b) phantom \<Rightarrow> 'b" 
    13 primrec of_phantom :: "('a, 'b) phantom \<Rightarrow> 'b" 
    14 where "of_phantom (phantom x) = x"
    14 where "of_phantom (phantom x) = x"
    15 
    15 
    16 lemma of_phantom_phantom [simp]: "phantom (of_phantom x) = x"
    16 lemma of_phantom_phantom [simp]: "phantom (of_phantom x) = x"