equal
deleted
inserted
replaced
75 by (rule t_eq) |
75 by (rule t_eq) |
76 |
76 |
77 print_quotients |
77 print_quotients |
78 |
78 |
79 ML {* |
79 ML {* |
80 Toplevel.context_of; |
|
81 Toplevel.keep |
|
82 *} |
|
83 |
|
84 ML {* |
|
85 get_fun repF [(@{typ qt}, @{typ qt})] @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"} |
80 get_fun repF [(@{typ qt}, @{typ qt})] @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"} |
86 |> fst |
|
87 |> Syntax.string_of_term @{context} |
81 |> Syntax.string_of_term @{context} |
88 |> writeln |
82 |> writeln |
89 *} |
83 *} |
90 |
84 |
91 ML {* |
85 ML {* |
92 get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "qt * nat"} |
86 get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "qt * nat"} |
93 |> fst |
|
94 |> Syntax.string_of_term @{context} |
87 |> Syntax.string_of_term @{context} |
95 |> writeln |
88 |> writeln |
96 *} |
89 *} |
97 |
90 |
98 ML {* |
91 ML {* |
99 get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |
92 get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |
100 |> fst |
|
101 |> Syntax.pretty_term @{context} |
93 |> Syntax.pretty_term @{context} |
102 |> Pretty.string_of |
94 |> Pretty.string_of |
103 |> writeln |
95 |> writeln |
104 *} |
96 *} |
105 |
97 |