equal
deleted
inserted
replaced
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}" |