src/CCL/Type.thy
changeset 81011 6d34c2bedaa3
parent 80917 2a77bc3b4eac
child 81091 c007e6d9941d
equal deleted inserted replaced
81010:5ea48342e0ae 81011:6d34c2bedaa3
    13   where "Subtype(A, P) == {x. x:A \<and> P(x)}"
    13   where "Subtype(A, P) == {x. x:A \<and> P(x)}"
    14 
    14 
    15 syntax
    15 syntax
    16   "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Subtype\<close>\<close>{_: _ ./ _})\<close>)
    16   "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix Subtype\<close>\<close>{_: _ ./ _})\<close>)
    17 syntax_consts
    17 syntax_consts
    18   "_Subtype" == Subtype
    18   Subtype
    19 translations
    19 translations
    20   "{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)"
    20   "{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)"
    21 
    21 
    22 definition Unit :: "i set"
    22 definition Unit :: "i set"
    23   where "Unit == {x. x=one}"
    23   where "Unit == {x. x=one}"