equal
deleted
inserted
replaced
9 begin |
9 begin |
10 |
10 |
11 notation |
11 notation |
12 rel_conj (infixr "OOO" 75) and |
12 rel_conj (infixr "OOO" 75) and |
13 map_fun (infixr "--->" 55) and |
13 map_fun (infixr "--->" 55) and |
14 fun_rel (infixr "===>" 55) |
14 rel_fun (infixr "===>" 55) |
15 |
15 |
16 end |
16 end |