equal
deleted
inserted
replaced
118 quotient ql = "'a list" / "Rl" |
118 quotient ql = "'a list" / "Rl" |
119 by (rule Rl_eq) |
119 by (rule Rl_eq) |
120 |
120 |
121 ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *} |
121 ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *} |
122 ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *} |
122 ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *} |
123 ML {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a list \<Rightarrow> ?'a list"})) *} |
123 ML {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a ql \<Rightarrow> ?'a ql"})) *} |
124 |
124 |
125 ML {* |
125 ML {* |
126 get_fun absF [(al, aq)] @{context} ttt |
126 fst (get_fun absF [(aq, al)] @{context} ttt) |
127 |> fst |
127 |> cterm_of @{theory} |
128 |> Syntax.pretty_term @{context} |
128 *} |
129 |> Pretty.string_of |
129 |
130 |> writeln |
130 ML {* val ttt2 = snd (dest_Free (term_of @{cpat "f :: nat ql \<Rightarrow> bool ql \<Rightarrow> 'a ql"})) *} |
131 *} |
131 |
132 |
132 ML {* |
133 |
133 fst (get_fun absF [(aq, al), (@{typ "nat ql"}, @{typ "nat list"}), (@{typ "bool ql"}, @{typ "bool list"})] @{context} ttt2) |
134 ML {* val ttt2 = snd (dest_Free (term_of @{cpat "f :: nat list \<Rightarrow> nat list"})) *} |
134 |> cterm_of @{theory} |
135 |
|
136 ML {* |
|
137 get_fun absF [(al, aq)] @{context} ttt2 |
|
138 |> fst |
|
139 |> Syntax.pretty_term @{context} |
|
140 |> Pretty.string_of |
|
141 |> writeln |
|
142 *} |
135 *} |
143 |
136 |
144 quotient_def (for qt) |
137 quotient_def (for qt) |
145 VR ::"string \<Rightarrow> qt" |
138 VR ::"string \<Rightarrow> qt" |
146 where |
139 where |