166 |
166 |
167 "----------- fun go ----------------------------------------------"; |
167 "----------- fun go ----------------------------------------------"; |
168 "----------- fun go ----------------------------------------------"; |
168 "----------- fun go ----------------------------------------------"; |
169 "----------- fun go ----------------------------------------------"; |
169 "----------- fun go ----------------------------------------------"; |
170 (* |
170 (* |
171 > val t = (Thm.term_of o the o (TermC.parse thy)) "a+b"; |
171 > val t = TermC.parseNEW'' thy "a+b"; |
172 val it = Const (#,#) $ Free (#,#) $ Free ("b", "RealDef.real") : term |
172 val it = Const (#,#) $ Free (#,#) $ Free ("b", "RealDef.real") : term |
173 > val plus_a = TermC.sub_at [L] t; |
173 > val plus_a = TermC.sub_at [L] t; |
174 > val b = TermC.sub_at [R] t; |
174 > val b = TermC.sub_at [R] t; |
175 > val plus = TermC.sub_at [L,L] t; |
175 > val plus = TermC.sub_at [L,L] t; |
176 > val a = TermC.sub_at [L,R] t; |
176 > val a = TermC.sub_at [L,R] t; |
177 |
177 |
178 > val t = (Thm.term_of o the o (TermC.parse thy)) "a+b+c"; |
178 > val t = TermC.parseNEW'' thy "a+b+c"; |
179 val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c", "RealDef.real") : term |
179 val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c", "RealDef.real") : term |
180 > val pl_pl_a_b = TermC.sub_at [L] t; |
180 > val pl_pl_a_b = TermC.sub_at [L] t; |
181 > val c = TermC.sub_at [R] t; |
181 > val c = TermC.sub_at [R] t; |
182 > val a = TermC.sub_at [L,R,L,R] t; |
182 > val a = TermC.sub_at [L,R,L,R] t; |
183 > val b = TermC.sub_at [L,R,R] t; |
183 > val b = TermC.sub_at [L,R,R] t; |
192 Free ("eqs_", "bool List.list")] : term list |
192 Free ("eqs_", "bool List.list")] : term list |
193 *) |
193 *) |
194 "----------- fun dsc_valT ----------------------------------------"; |
194 "----------- fun dsc_valT ----------------------------------------"; |
195 "----------- fun dsc_valT ----------------------------------------"; |
195 "----------- fun dsc_valT ----------------------------------------"; |
196 "----------- fun dsc_valT ----------------------------------------"; |
196 "----------- fun dsc_valT ----------------------------------------"; |
197 (*> val t = (Thm.term_of o the o (TermC.parse thy)) "equality"; |
197 (*> val t = TermC.parseNEW'' thy "equality"; |
198 > val T = type_of t; |
198 > val T = type_of t; |
199 val T = "bool => Tools.una" : typ |
199 val T = "bool => Tools.una" : typ |
200 > val dsc = dsc_valT t; |
200 > val dsc = dsc_valT t; |
201 val dsc = "una" : string |
201 val dsc = "una" : string |
202 |
202 |
203 > val t = (Thm.term_of o the o (TermC.parse thy)) "fixedValues"; |
203 > val t = TermC.parseNEW'' thy "fixedValues"; |
204 > val T = type_of t; |
204 > val T = type_of t; |
205 val T = "bool List.list => Tools.nam" : typ |
205 val T = "bool List.list => Tools.nam" : typ |
206 > val dsc = dsc_valT t; |
206 > val dsc = dsc_valT t; |
207 val dsc = "nam" : string*) |
207 val dsc = "nam" : string*) |
208 "----------- fun arguments_from_model ---------------------------------------"; |
208 "----------- fun arguments_from_model ---------------------------------------"; |