78 |
78 |
79 syntax |
79 syntax |
80 |
80 |
81 "~=" :: ['a, 'a] => bool (infixl 50) |
81 "~=" :: ['a, 'a] => bool (infixl 50) |
82 |
82 |
83 "@Eps" :: [pttrn, bool] => 'a ("(3@ _./ _)" 10) |
83 "@Eps" :: [pttrn, bool] => 'a ("(3@ _./ _)" [0, 10] 10) |
84 |
84 |
85 (* Alternative Quantifiers *) |
85 (* Alternative Quantifiers *) |
86 |
86 |
87 "*All" :: [idts, bool] => bool ("(3ALL _./ _)" 10) |
87 "*All" :: [idts, bool] => bool ("(3ALL _./ _)" [0, 10] 10) |
88 "*Ex" :: [idts, bool] => bool ("(3EX _./ _)" 10) |
88 "*Ex" :: [idts, bool] => bool ("(3EX _./ _)" [0, 10] 10) |
89 "*Ex1" :: [idts, bool] => bool ("(3EX! _./ _)" 10) |
89 "*Ex1" :: [idts, bool] => bool ("(3EX! _./ _)" [0, 10] 10) |
90 |
90 |
91 (* Let expressions *) |
91 (* Let expressions *) |
92 |
92 |
93 "_bind" :: [pttrn, 'a] => letbind ("(2_ =/ _)" 10) |
93 "_bind" :: [pttrn, 'a] => letbind ("(2_ =/ _)" 10) |
94 "" :: letbind => letbinds ("_") |
94 "" :: letbind => letbinds ("_") |
117 "op &" :: [bool, bool] => bool (infixr "\\<and>" 35) |
117 "op &" :: [bool, bool] => bool (infixr "\\<and>" 35) |
118 "op |" :: [bool, bool] => bool (infixr "\\<or>" 30) |
118 "op |" :: [bool, bool] => bool (infixr "\\<or>" 30) |
119 "op -->" :: [bool, bool] => bool (infixr "\\<midarrow>\\<rightarrow>" 25) |
119 "op -->" :: [bool, bool] => bool (infixr "\\<midarrow>\\<rightarrow>" 25) |
120 "op o" :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl "\\<circ>" 55) |
120 "op o" :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl "\\<circ>" 55) |
121 "op ~=" :: ['a, 'a] => bool (infixl "\\<noteq>" 50) |
121 "op ~=" :: ['a, 'a] => bool (infixl "\\<noteq>" 50) |
122 "@Eps" :: [pttrn, bool] => 'a ("(3\\<epsilon>_./ _)" 10) |
122 "@Eps" :: [pttrn, bool] => 'a ("(3\\<epsilon>_./ _)" [0, 10] 10) |
123 "! " :: [idts, bool] => bool ("(3\\<forall>_./ _)" 10) |
123 "! " :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10) |
124 "? " :: [idts, bool] => bool ("(3\\<exists>_./ _)" 10) |
124 "? " :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10) |
125 "?! " :: [idts, bool] => bool ("(3\\<exists>!_./ _)" 10) |
125 "?! " :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10) |
126 "*All" :: [idts, bool] => bool ("(3\\<forall>_./ _)" 10) |
126 "*All" :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10) |
127 "*Ex" :: [idts, bool] => bool ("(3\\<exists>_./ _)" 10) |
127 "*Ex" :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10) |
128 "*Ex1" :: [idts, bool] => bool ("(3\\<exists>!_./ _)" 10) |
128 "*Ex1" :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10) |
129 "@case1" :: ['a, 'b] => case_syn ("(2_ \\<mapsto>/ _)" 10) |
129 "@case1" :: ['a, 'b] => case_syn ("(2_ \\<mapsto>/ _)" 10) |
130 |
130 |
131 |
131 |
132 |
132 |
133 (** Rules and definitions **) |
133 (** Rules and definitions **) |