equal
deleted
inserted
replaced
18 ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10) |
18 ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10) |
19 |
19 |
20 "_case_syntax":: "['a, cases_syn] => 'b" |
20 "_case_syntax":: "['a, cases_syn] => 'b" |
21 ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10) |
21 ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10) |
22 |
22 |
23 (* should become standard syntax once x-symbols supports it *) |
|
24 syntax (latex) |
|
25 nexists :: "('a => bool) => bool" (binder "\<nexists>" 10) |
|
26 translations |
|
27 "\<nexists>x. P" <= "\<not>(\<exists>x. P)" |
|
28 |
23 |
29 (* SETS *) |
24 (* SETS *) |
30 |
25 |
31 (* empty set *) |
26 (* empty set *) |
32 notation (latex) |
27 notation (latex) |