equal
deleted
inserted
replaced
228 |
228 |
229 typedef ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set" |
229 typedef ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set" |
230 unfolding prod_def by auto |
230 unfolding prod_def by auto |
231 |
231 |
232 type_notation (xsymbols) |
232 type_notation (xsymbols) |
233 "prod" ("(_ \<times>/ _)" [21, 20] 20) |
|
234 type_notation (HTML output) |
|
235 "prod" ("(_ \<times>/ _)" [21, 20] 20) |
233 "prod" ("(_ \<times>/ _)" [21, 20] 20) |
236 |
234 |
237 definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where |
235 definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where |
238 "Pair a b = Abs_prod (Pair_Rep a b)" |
236 "Pair a b = Abs_prod (Pair_Rep a b)" |
239 |
237 |
1007 "A <*> B == Sigma A (%_. B)" |
1005 "A <*> B == Sigma A (%_. B)" |
1008 |
1006 |
1009 notation (xsymbols) |
1007 notation (xsymbols) |
1010 Times (infixr "\<times>" 80) |
1008 Times (infixr "\<times>" 80) |
1011 |
1009 |
1012 notation (HTML output) |
|
1013 Times (infixr "\<times>" 80) |
|
1014 |
|
1015 hide_const (open) Times |
1010 hide_const (open) Times |
1016 |
1011 |
1017 syntax |
1012 syntax |
1018 "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10) |
1013 "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10) |
1019 translations |
1014 translations |