equal
deleted
inserted
replaced
21 *) |
21 *) |
22 |
22 |
23 notation (latex output) |
23 notation (latex output) |
24 rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and |
24 rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and |
25 pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and |
25 pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and |
26 "op -->" (infix "\<longrightarrow>" 100) and |
26 implies (infix "\<longrightarrow>" 100) and |
27 "==>" (infix "\<Longrightarrow>" 100) and |
27 "==>" (infix "\<Longrightarrow>" 100) and |
28 fun_map ("_ \<singlearr> _" 51) and |
28 fun_map ("_ \<singlearr> _" 51) and |
29 fun_rel ("_ \<doublearr> _" 51) and |
29 fun_rel ("_ \<doublearr> _" 51) and |
30 list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *) |
30 list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *) |
31 fempty ("\<emptyset>") and |
31 fempty ("\<emptyset>") and |