121 "op ~=" :: ['a, 'a] => bool (infixl "\\<noteq>" 50) |
121 "op ~=" :: ['a, 'a] => bool (infixl "\\<noteq>" 50) |
122 "@Eps" :: [pttrn, bool] => 'a ("(3\\<epsilon>_./ _)" [0, 10] 10) |
122 "@Eps" :: [pttrn, bool] => 'a ("(3\\<epsilon>_./ _)" [0, 10] 10) |
123 "! " :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10) |
123 "! " :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10) |
124 "? " :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10) |
124 "? " :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10) |
125 "?! " :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10) |
125 "?! " :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10) |
|
126 "@case1" :: ['a, 'b] => case_syn ("(2_ \\<mapsto>/ _)" 10) |
|
127 |
|
128 syntax (symbols output) |
126 "*All" :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10) |
129 "*All" :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10) |
127 "*Ex" :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10) |
130 "*Ex" :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10) |
128 "*Ex1" :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10) |
131 "*Ex1" :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10) |
129 "@case1" :: ['a, 'b] => case_syn ("(2_ \\<mapsto>/ _)" 10) |
132 |
130 |
133 |
131 |
134 |
132 |
135 |
133 (** Rules and definitions **) |
136 (** Rules and definitions **) |
134 |
137 |