equal
deleted
inserted
replaced
12 axioms t_eq: "EQUIV Rt" |
12 axioms t_eq: "EQUIV Rt" |
13 |
13 |
14 quotient qt = "t" / "Rt" |
14 quotient qt = "t" / "Rt" |
15 by (rule t_eq) |
15 by (rule t_eq) |
16 |
16 |
17 setup {* |
|
18 maps_update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #> |
|
19 maps_update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #> |
|
20 maps_update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} |
|
21 *} |
|
22 |
|
23 |
|
24 ML {* |
17 ML {* |
25 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"} |
18 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"} |
26 |> fst |
19 |> fst |
27 |> Syntax.string_of_term @{context} |
20 |> Syntax.string_of_term @{context} |
28 |> writeln |
21 |> writeln*) |
29 *} |
22 *} |
30 |
23 |
31 ML {* |
24 ML {* |
32 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"} |
25 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"} |
33 |> fst |
26 |> fst |