184 "----------- inst_bdv -----------------------------------"; |
184 "----------- inst_bdv -----------------------------------"; |
185 if (UnparseC.term o Thm.prop_of) @{thm d1_isolate_add2} = |
185 if (UnparseC.term o Thm.prop_of) @{thm d1_isolate_add2} = |
186 "\<not> ?bdv occurs_in ?a \<Longrightarrow>\n(?a + ?bdv = 0) = (?bdv = - 1 * ?a)" |
186 "\<not> ?bdv occurs_in ?a \<Longrightarrow>\n(?a + ?bdv = 0) = (?bdv = - 1 * ?a)" |
187 then () |
187 then () |
188 else error "termC.sml d1_isolate_add2"; |
188 else error "termC.sml d1_isolate_add2"; |
189 val subst = [(TermC.str2term "bdv", TermC.str2term "x")]; |
189 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]; |
190 val t = (Eval.norm o Thm.prop_of) @{thm d1_isolate_add2}; |
190 val t = (Eval.norm o Thm.prop_of) @{thm d1_isolate_add2}; |
191 val t' = TermC.inst_bdv subst t; |
191 val t' = TermC.inst_bdv subst t; |
192 if UnparseC.term t' = "\<not> x occurs_in ?a \<Longrightarrow> (?a + x = 0) = (x = - 1 * ?a)" |
192 if UnparseC.term t' = "\<not> x occurs_in ?a \<Longrightarrow> (?a + x = 0) = (x = - 1 * ?a)" |
193 then () |
193 then () |
194 else error "termC.sml inst_bdv 1"; |
194 else error "termC.sml inst_bdv 1"; |
197 "?bdv_4.0] occur_exactly_in ?a \<Longrightarrow>\n(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)" |
197 "?bdv_4.0] occur_exactly_in ?a \<Longrightarrow>\n(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)" |
198 then () else error "termC.sml separate_bdvs_add"; |
198 then () else error "termC.sml separate_bdvs_add"; |
199 (*default_print_depth 5;*) |
199 (*default_print_depth 5;*) |
200 |
200 |
201 val subst = |
201 val subst = |
202 [(TermC.str2term "bdv_1", TermC.str2term "c"), |
202 [(TermC.parse_test @{context} "bdv_1", TermC.parse_test @{context} "c"), |
203 (TermC.str2term "bdv_2", TermC.str2term "c_2"), |
203 (TermC.parse_test @{context} "bdv_2", TermC.parse_test @{context} "c_2"), |
204 (TermC.str2term "bdv_3", TermC.str2term "c_3"), |
204 (TermC.parse_test @{context} "bdv_3", TermC.parse_test @{context} "c_3"), |
205 (TermC.str2term "bdv_4", TermC.str2term "c_4")]; |
205 (TermC.parse_test @{context} "bdv_4", TermC.parse_test @{context} "c_4")]; |
206 val t = (Eval.norm o Thm.prop_of) @{thm separate_bdvs_add}; |
206 val t = (Eval.norm o Thm.prop_of) @{thm separate_bdvs_add}; |
207 val t' = TermC.inst_bdv subst t; |
207 val t' = TermC.inst_bdv subst t; |
208 |
208 |
209 if UnparseC.term t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a \<Longrightarrow>\n" ^ |
209 if UnparseC.term t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a \<Longrightarrow>\n" ^ |
210 "(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)" |
210 "(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)" |
211 then () else error "termC.sml inst_bdv 2"; |
211 then () else error "termC.sml inst_bdv 2"; |
212 |
212 |
213 "----------- subst_atomic_all ---------------------------"; |
213 "----------- subst_atomic_all ---------------------------"; |
214 "----------- subst_atomic_all ---------------------------"; |
214 "----------- subst_atomic_all ---------------------------"; |
215 "----------- subst_atomic_all ---------------------------"; |
215 "----------- subst_atomic_all ---------------------------"; |
216 val t = TermC.str2term "(tl vs_vs) from vs_vs occur_exactly_in (NTH 1 (es_es::bool list))"; |
216 val t = TermC.parse_test @{context} "(tl vs_vs) from vs_vs occur_exactly_in (NTH 1 (es_es::bool list))"; |
217 val env = [(TermC.str2term "vs_vs::real list", TermC.str2term "[c, c_2]"), |
217 val env = [(TermC.parse_test @{context} "vs_vs::real list", TermC.parse_test @{context} "[c, c_2]"), |
218 (TermC.str2term "es_es::bool list", TermC.str2term "[c_2 = 0, c + c_2 = 1]")]; |
218 (TermC.parse_test @{context} "es_es::bool list", TermC.parse_test @{context} "[c_2 = 0, c + c_2 = 1]")]; |
219 val (all_Free_subst, t') = TermC.subst_atomic_all env t; |
219 val (all_Free_subst, t') = TermC.subst_atomic_all env t; |
220 |
220 |
221 if all_Free_subst andalso |
221 if all_Free_subst andalso |
222 UnparseC.term t' = "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1 [c_2 = 0, c + c_2 = 1]" |
222 UnparseC.term t' = "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1 [c_2 = 0, c + c_2 = 1]" |
223 then () |
223 then () |
229 else error "TermC.subst_atomic_all should be 'false'"; |
229 else error "TermC.subst_atomic_all should be 'false'"; |
230 |
230 |
231 "----------- Pattern.match ------------------------------"; |
231 "----------- Pattern.match ------------------------------"; |
232 "----------- Pattern.match ------------------------------"; |
232 "----------- Pattern.match ------------------------------"; |
233 "----------- Pattern.match ------------------------------"; |
233 "----------- Pattern.match ------------------------------"; |
234 val t = TermC.str2term "3 * x\<up>2 = (1::real)"; |
234 val t = TermC.parse_test @{context} "3 * x\<up>2 = (1::real)"; |
235 val pat = (TermC.free2var o TermC.str2term) "a * b\<up>2 = (c::real)"; |
235 val pat = (TermC.free2var o TermC.parse_test @{context}) "a * b\<up>2 = (c::real)"; |
236 (* ! \<up> \<up> ^^!... necessary for Pattern.match, see Logic.varify_global below*) |
236 (* ! \<up> \<up> ^^!... necessary for Pattern.match, see Logic.varify_global below*) |
237 val insts = Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty); |
237 val insts = Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty); |
238 (*default_print_depth 3; 999*) insts; |
238 (*default_print_depth 3; 999*) insts; |
239 (*val insts = |
239 (*val insts = |
240 ({}, |
240 ({}, |
241 {(("a", 0), ("Real.real", Free ("3", "Real.real"))), |
241 {(("a", 0), ("Real.real", Free ("3", "Real.real"))), |
242 (("b", 0), ("Real.real", Free ("x", "Real.real"))), |
242 (("b", 0), ("Real.real", Free ("x", "Real.real"))), |
243 (("c", 0), ("Real.real", Free ("1", "Real.real")))})*) |
243 (("c", 0), ("Real.real", Free ("1", "Real.real")))})*) |
244 |
244 |
245 "----- throws exn MATCH..."; |
245 "----- throws exn MATCH..."; |
246 (* val t = TermC.str2term "x"; |
246 (* val t = TermC.parse_test @{context} "x"; |
247 (Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty)) |
247 (Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty)) |
248 handle MATCH => ???; *) |
248 handle MATCH => ???; *) |
249 |
249 |
250 val thy = @{theory "Complex_Main"}; |
250 val thy = @{theory "Complex_Main"}; |
251 val PARSE = Syntax.read_term_global thy; |
251 val PARSE = Syntax.read_term_global thy; |
281 val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"}; (*<<<<<<<---------------*) |
281 val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"}; (*<<<<<<<---------------*) |
282 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 1" |
282 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 1" |
283 else (); |
283 else (); |
284 |
284 |
285 "----- test 2: Nok"; |
285 "----- test 2: Nok"; |
286 val pa = Logic.varify_global (TermC.str2term "a = (0::real)");(*<<<<<<<-------------*) |
286 val pa = Logic.varify_global (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*) |
287 tracing "paLo2=..."; TermC.atomty pa; tracing "...=paLo2"; |
287 tracing "paLo2=..."; TermC.atomty pa; tracing "...=paLo2"; |
288 (*** |
288 (*** |
289 *** Const (op =, real => real => bool) |
289 *** Const (op =, real => real => bool) |
290 *** . Var ((a, 0), real) |
290 *** . Var ((a, 0), real) |
291 *** . Var ((0, 0), real) |
291 *** . Var ((0, 0), real) |
292 ***) |
292 ***) |
293 "----- test 2a true"; |
293 "----- test 2a true"; |
294 val tm = TermC.str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*) |
294 val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*) |
295 if TermC.matches thy tm pa then () |
295 if TermC.matches thy tm pa then () |
296 else error "termC.sml diff.behav. in TermC.matches true 2"; |
296 else error "termC.sml diff.behav. in TermC.matches true 2"; |
297 "----- test 2b false"; |
297 "----- test 2b false"; |
298 val tm = TermC.str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*) |
298 val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*) |
299 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 2" |
299 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 2" |
300 else (); |
300 else (); |
301 (* i.e. !!!!!!!!!!!!!!!!! THIS KIND OF PATTERN IS NOT RELIABLE !!!!!!!!!!!!!!!!! |
301 (* i.e. !!!!!!!!!!!!!!!!! THIS KIND OF PATTERN IS NOT RELIABLE !!!!!!!!!!!!!!!!! |
302 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 2" |
302 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 2" |
303 else ();*) |
303 else ();*) |
304 |
304 |
305 "----- test 3: OK"; |
305 "----- test 3: OK"; |
306 val pa = TermC.free2var (TermC.str2term "a = (0::real)");(*<<<<<<<-------------*) |
306 val pa = TermC.free2var (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*) |
307 tracing "paF2=..."; TermC.atomty pa; tracing "...=paF2"; |
307 tracing "paF2=..."; TermC.atomty pa; tracing "...=paF2"; |
308 (*** |
308 (*** |
309 *** Const (op =, real => real => bool) |
309 *** Const (op =, real => real => bool) |
310 *** . Var ((a, 0), real) |
310 *** . Var ((a, 0), real) |
311 *** . Free (0, real) |
311 *** . Free (0, real) |
312 ***) |
312 ***) |
313 "----- test 3a true"; |
313 "----- test 3a true"; |
314 val tm = TermC.str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*) |
314 val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*) |
315 if TermC.matches thy tm pa then () |
315 if TermC.matches thy tm pa then () |
316 else error "termC.sml diff.behav. in TermC.matches true 3"; |
316 else error "termC.sml diff.behav. in TermC.matches true 3"; |
317 "----- test 3b false"; |
317 "----- test 3b false"; |
318 val tm = TermC.str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*) |
318 val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*) |
319 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 3" |
319 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 3" |
320 else (); |
320 else (); |
321 |
321 |
322 "----- test 4=3 with specific data"; |
322 "----- test 4=3 with specific data"; |
323 val pa = TermC.free2var (TermC.str2term "M_b 0"); |
323 val pa = TermC.free2var (TermC.parse_test @{context} "M_b 0"); |
324 "----- test 4a true"; |
324 "----- test 4a true"; |
325 val tm = TermC.str2term "M_b 0"; |
325 val tm = TermC.parse_test @{context} "M_b 0"; |
326 if TermC.matches thy tm pa then () |
326 if TermC.matches thy tm pa then () |
327 else error "termC.sml diff.behav. in TermC.matches true 4"; |
327 else error "termC.sml diff.behav. in TermC.matches true 4"; |
328 "----- test 4b false"; |
328 "----- test 4b false"; |
329 val tm = TermC.str2term "M_b x"; |
329 val tm = TermC.parse_test @{context} "M_b x"; |
330 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 4" |
330 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 4" |
331 else (); |
331 else (); |
332 |
332 |
333 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------"; |
333 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------"; |
334 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------"; |
334 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------"; |
535 *) |
535 *) |
536 |
536 |
537 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------"; |
537 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------"; |
538 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------"; |
538 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------"; |
539 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------"; |
539 "----------- fun TermC.is_bdv_subst ------------------------------------------------------------------"; |
540 if TermC.is_bdv_subst (TermC.str2term "[(''bdv'', v_v)]") then () |
540 if TermC.is_bdv_subst (TermC.parse_test @{context} "[(''bdv'', v_v)]") then () |
541 else error "TermC.is_bdv_subst canged 1"; |
541 else error "TermC.is_bdv_subst canged 1"; |
542 |
542 |
543 if TermC.is_bdv_subst (TermC.str2term "[(''bdv_1'', v_s1),(''bdv_2'', v_s2)]") then () |
543 if TermC.is_bdv_subst (TermC.parse_test @{context} "[(''bdv_1'', v_s1),(''bdv_2'', v_s2)]") then () |
544 else error "TermC.is_bdv_subst canged 2"; |
544 else error "TermC.is_bdv_subst canged 2"; |
545 |
545 |
546 "----------- fun str_of_int --------------------------------------------------------------------"; |
546 "----------- fun str_of_int --------------------------------------------------------------------"; |
547 "----------- fun str_of_int --------------------------------------------------------------------"; |
547 "----------- fun str_of_int --------------------------------------------------------------------"; |
548 "----------- fun str_of_int --------------------------------------------------------------------"; |
548 "----------- fun str_of_int --------------------------------------------------------------------"; |
579 case ThmC_Def.int_opt_of_string "#123" of |
579 case ThmC_Def.int_opt_of_string "#123" of |
580 NONE => () | _ => raise error "ThmC_Def.int_opt_of_string #123 changed"; |
580 NONE => () | _ => raise error "ThmC_Def.int_opt_of_string #123 changed"; |
581 case ThmC_Def.int_opt_of_string "-123" of |
581 case ThmC_Def.int_opt_of_string "-123" of |
582 SOME ~123 => () | _ => raise error "ThmC_Def.int_opt_of_string -123 changed"; |
582 SOME ~123 => () | _ => raise error "ThmC_Def.int_opt_of_string -123 changed"; |
583 |
583 |
584 val t = TermC.str2term "1"; |
584 val t = TermC.parse_test @{context} "1"; |
585 if TermC.is_num t = true then () else error "TermC.is_num 1"; |
585 if TermC.is_num t = true then () else error "TermC.is_num 1"; |
586 |
586 |
587 val t = TermC.str2term "-1"; |
587 val t = TermC.parse_test @{context} "-1"; |
588 if TermC.is_num t = true then () else error "TermC.is_num -1"; |
588 if TermC.is_num t = true then () else error "TermC.is_num -1"; |
589 |
589 |
590 val t = TermC.str2term "a123"; |
590 val t = TermC.parse_test @{context} "a123"; |
591 if TermC.is_num t = false then () else error "TermC.is_num a123"; |
591 if TermC.is_num t = false then () else error "TermC.is_num a123"; |
592 |
592 |
593 "----------- fun TermC.is_f_x ------------------------------------------------------------------------"; |
593 "----------- fun TermC.is_f_x ------------------------------------------------------------------------"; |
594 "----------- fun TermC.is_f_x ------------------------------------------------------------------------"; |
594 "----------- fun TermC.is_f_x ------------------------------------------------------------------------"; |
595 "----------- fun TermC.is_f_x ------------------------------------------------------------------------"; |
595 "----------- fun TermC.is_f_x ------------------------------------------------------------------------"; |
596 val t = TermC.str2term "q_0/2 * L * x"; |
596 val t = TermC.parse_test @{context} "q_0/2 * L * x"; |
597 if TermC.is_f_x t = false then () else error "TermC.is_f_x q_0/2 * L * x"; |
597 if TermC.is_f_x t = false then () else error "TermC.is_f_x q_0/2 * L * x"; |
598 |
598 |
599 val t = TermC.str2term "M_b x"; |
599 val t = TermC.parse_test @{context} "M_b x"; |
600 if TermC.is_f_x t = true then () else error "M_b x"; |
600 if TermC.is_f_x t = true then () else error "M_b x"; |
601 |
601 |
602 "----------- fun list2isalist, fun isalist2list ------------------------------------------------"; |
602 "----------- fun list2isalist, fun isalist2list ------------------------------------------------"; |
603 "----------- fun list2isalist, fun isalist2list ------------------------------------------------"; |
603 "----------- fun list2isalist, fun isalist2list ------------------------------------------------"; |
604 "----------- fun list2isalist, fun isalist2list ------------------------------------------------"; |
604 "----------- fun list2isalist, fun isalist2list ------------------------------------------------"; |
605 val t = TermC.str2term "R=(R::real)"; |
605 val t = TermC.parse_test @{context} "R=(R::real)"; |
606 val T = type_of t; |
606 val T = type_of t; |
607 val ss = TermC.list2isalist T [t,t,t]; |
607 val ss = TermC.list2isalist T [t,t,t]; |
608 if UnparseC.term ss = "[R = R, R = R, R = R]" then () else error "list2isalist 1"; |
608 if UnparseC.term ss = "[R = R, R = R, R = R]" then () else error "list2isalist 1"; |
609 |
609 |
610 val t = TermC.str2term "[a=b,c=d,e=f]"; |
610 val t = TermC.parse_test @{context} "[a=b,c=d,e=f]"; |
611 val il = TermC.isalist2list t; |
611 val il = TermC.isalist2list t; |
612 if UnparseC.terms il = "[\"a = b\", \"c = d\", \"e = f\"]" then () else error "isalist2list 2"; |
612 if UnparseC.terms il = "[\"a = b\", \"c = d\", \"e = f\"]" then () else error "isalist2list 2"; |
613 |
613 |
614 val t = TermC.str2term "[a=b,c=d,e=f]"; |
614 val t = TermC.parse_test @{context} "[a=b,c=d,e=f]"; |
615 val il = TermC.isalist2list t; |
615 val il = TermC.isalist2list t; |
616 if UnparseC.terms il = "[\"a = b\", \"c = d\", \"e = f\"]" then () else error "isalist2list 3"; |
616 if UnparseC.terms il = "[\"a = b\", \"c = d\", \"e = f\"]" then () else error "isalist2list 3"; |
617 |
617 |
618 val t = TermC.str2term "ss___s::bool list"; |
618 val t = TermC.parse_test @{context} "ss___s::bool list"; |
619 (TermC.isalist2list t; error "isalist2list 1") handle TERM ("isalist2list applied to NON-list: ", _) =>(); |
619 (TermC.isalist2list t; error "isalist2list 1") handle TERM ("isalist2list applied to NON-list: ", _) =>(); |
620 |
620 |
621 "----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------"; |
621 "----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------"; |
622 "----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------"; |
622 "----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------"; |
623 "----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------"; |
623 "----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------"; |
645 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------"; |
645 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------"; |
646 val T = type_of (TermC.parseNEW' ctxt "12::real"); |
646 val T = type_of (TermC.parseNEW' ctxt "12::real"); |
647 val t = TermC.mk_factroot "SqRoot.sqrt" T 2 3; |
647 val t = TermC.mk_factroot "SqRoot.sqrt" T 2 3; |
648 if UnparseC.term t = "2 * ??.SqRoot.sqrt 3" then () else error "mk_factroot"; |
648 if UnparseC.term t = "2 * ??.SqRoot.sqrt 3" then () else error "mk_factroot"; |
649 |
649 |
650 val t = TermC.str2term "aaa + bbb"; |
650 val t = TermC.parse_test @{context} "aaa + bbb"; |
651 val op_ as Const (\<^const_name>\<open>plus\<close>, Top) $ Free ("aaa", T1) $ Free ("bbb", T2) = t; |
651 val op_ as Const (\<^const_name>\<open>plus\<close>, Top) $ Free ("aaa", T1) $ Free ("bbb", T2) = t; |
652 val t' = TermC.mk_num_op_num T1 T2 (\<^const_name>\<open>plus\<close>, Top) 2 3; |
652 val t' = TermC.mk_num_op_num T1 T2 (\<^const_name>\<open>plus\<close>, Top) 2 3; |
653 if UnparseC.term t' = "2 + 3" then () else error "mk_num_op_num"; |
653 if UnparseC.term t' = "2 + 3" then () else error "mk_num_op_num"; |
654 |
654 |
655 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------"; |
655 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------"; |
662 |
662 |
663 "----------- fun TermC.is_list -----------------------------------------------------------------------"; |
663 "----------- fun TermC.is_list -----------------------------------------------------------------------"; |
664 "----------- fun TermC.is_list -----------------------------------------------------------------------"; |
664 "----------- fun TermC.is_list -----------------------------------------------------------------------"; |
665 "----------- fun TermC.is_list -----------------------------------------------------------------------"; |
665 "----------- fun TermC.is_list -----------------------------------------------------------------------"; |
666 val (SOME ct) = TermC.parseNEW ctxt "lll::real list"; |
666 val (SOME ct) = TermC.parseNEW ctxt "lll::real list"; |
667 val t = TermC.str2term "lll::real list"; |
667 val t = TermC.parse_test @{context} "lll::real list"; |
668 val ty = Term.type_of ct; |
668 val ty = Term.type_of ct; |
669 if TermC.is_list t = false then () else error "TermC.is_list lll::real list"; |
669 if TermC.is_list t = false then () else error "TermC.is_list lll::real list"; |
670 |
670 |
671 val t = TermC.str2term "[a, b, c]"; |
671 val t = TermC.parse_test @{context} "[a, b, c]"; |
672 val ty = Term.type_of ct; |
672 val ty = Term.type_of ct; |
673 if TermC.is_list t = true then () else error "TermC.is_list [a, b, c]"; |
673 if TermC.is_list t = true then () else error "TermC.is_list [a, b, c]"; |
674 |
674 |
675 "----------- fun mk_frac, proper term with uminus ----------------------------------------------"; |
675 "----------- fun mk_frac, proper term with uminus ----------------------------------------------"; |
676 "----------- fun mk_frac, proper term with uminus ----------------------------------------------"; |
676 "----------- fun mk_frac, proper term with uminus ----------------------------------------------"; |