equal
deleted
inserted
replaced
11 |
11 |
12 subsection \<open>Relator for function space\<close> |
12 subsection \<open>Relator for function space\<close> |
13 |
13 |
14 bundle lifting_syntax |
14 bundle lifting_syntax |
15 begin |
15 begin |
16 notation rel_fun (infixr \<open>===>\<close> 55) |
16 notation rel_fun (infixr \<open>===>\<close> 55) |
17 notation map_fun (infixr \<open>--->\<close> 55) |
17 notation map_fun (infixr \<open>--->\<close> 55) |
18 end |
18 end |
19 |
19 |
20 context includes lifting_syntax |
20 context includes lifting_syntax |
21 begin |
21 begin |
22 |
22 |