461 + Max: semilattice_order_set max greater_eq greater |
461 + Max: semilattice_order_set max greater_eq greater |
462 defines |
462 defines |
463 Min = Min.F and Max = Max.F .. |
463 Min = Min.F and Max = Max.F .. |
464 |
464 |
465 end |
465 end |
466 |
|
467 syntax (ASCII) |
|
468 "_MIN1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _./ _)" [0, 10] 10) |
|
469 "_MIN" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _:_./ _)" [0, 0, 10] 10) |
|
470 "_MAX1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _./ _)" [0, 10] 10) |
|
471 "_MAX" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _:_./ _)" [0, 0, 10] 10) |
|
472 |
|
473 syntax (output) |
|
474 "_MIN1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _./ _)" [0, 10] 10) |
|
475 "_MIN" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _:_./ _)" [0, 0, 10] 10) |
|
476 "_MAX1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _./ _)" [0, 10] 10) |
|
477 "_MAX" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _:_./ _)" [0, 0, 10] 10) |
|
478 |
466 |
479 syntax |
467 syntax |
480 "_MIN1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _./ _)" [0, 10] 10) |
468 "_MIN1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _./ _)" [0, 10] 10) |
481 "_MIN" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _\<in>_./ _)" [0, 0, 10] 10) |
469 "_MIN" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _\<in>_./ _)" [0, 0, 10] 10) |
482 "_MAX1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _./ _)" [0, 10] 10) |
470 "_MAX1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _./ _)" [0, 10] 10) |