src/HOL/Library/Phantom_Type.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Library/Phantom_Type.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Phantom_Type.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Andreas Lochbihler
     1.5  *)
     1.6  
     1.7 -section {* A generic phantom type *}
     1.8 +section \<open>A generic phantom type\<close>
     1.9  
    1.10  theory Phantom_Type
    1.11  imports Main
    1.12 @@ -21,14 +21,14 @@
    1.13  translations
    1.14    "Phantom('t)" => "CONST phantom :: _ \<Rightarrow> ('t, _) phantom"
    1.15  
    1.16 -typed_print_translation {*
    1.17 +typed_print_translation \<open>
    1.18    let
    1.19      fun phantom_tr' ctxt (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts =
    1.20            list_comb
    1.21              (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts)
    1.22        | phantom_tr' _ _ _ = raise Match;
    1.23    in [(@{const_syntax phantom}, phantom_tr')] end
    1.24 -*}
    1.25 +\<close>
    1.26  
    1.27  lemma of_phantom_inject [simp]:
    1.28    "of_phantom x = of_phantom y \<longleftrightarrow> x = y"