equal
deleted
inserted
replaced
17 class Inf = |
17 class Inf = |
18 fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>") |
18 fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>") |
19 |
19 |
20 class Sup = |
20 class Sup = |
21 fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>") |
21 fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>") |
22 |
|
23 syntax (ASCII) |
|
24 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10) |
|
25 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _:_./ _)" [0, 0, 10] 10) |
|
26 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _./ _)" [0, 10] 10) |
|
27 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _:_./ _)" [0, 0, 10] 10) |
|
28 |
22 |
29 syntax |
23 syntax |
30 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10) |
24 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10) |
31 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _\<in>_./ _)" [0, 0, 10] 10) |
25 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _\<in>_./ _)" [0, 0, 10] 10) |
32 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _./ _)" [0, 10] 10) |
26 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _./ _)" [0, 10] 10) |