equal
deleted
inserted
replaced
110 make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |
110 make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |
111 )) |> snd |
111 )) |> snd |
112 *} |
112 *} |
113 *) |
113 *) |
114 |
114 |
|
115 consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
|
116 axioms Rl_eq: "EQUIV Rl" |
|
117 |
|
118 quotient ql = "'a list" / "Rl" |
|
119 by (rule Rl_eq) |
|
120 |
|
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"})) *} |
|
123 ML {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a list \<Rightarrow> ?'a list"})) *} |
|
124 |
|
125 ML {* |
|
126 get_fun absF [(al, aq)] @{context} ttt |
|
127 |> fst |
|
128 |> Syntax.pretty_term @{context} |
|
129 |> Pretty.string_of |
|
130 |> writeln |
|
131 *} |
|
132 |
|
133 |
|
134 ML {* val ttt2 = snd (dest_Free (term_of @{cpat "f :: nat list \<Rightarrow> nat list"})) *} |
|
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 *} |
|
143 |
115 quotient_def (for qt) |
144 quotient_def (for qt) |
116 VR ::"string \<Rightarrow> qt" |
145 VR ::"string \<Rightarrow> qt" |
117 where |
146 where |
118 "VR \<equiv> vr" |
147 "VR \<equiv> vr" |
119 |
148 |