equal
deleted
inserted
replaced
357 val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge") |
357 val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge") |
358 val str = "x + z"; |
358 val str = "x + z"; |
359 TermC.parseNEW' ctxt str; |
359 TermC.parseNEW' ctxt str; |
360 |
360 |
361 "---------------"; |
361 "---------------"; |
|
362 val ctxt = @{context} |
362 val str = "x + 2*z"; |
363 val str = "x + 2*z"; |
363 val t = Syntax.read_term_global thy str; |
364 val t = Syntax.read_term_global thy str; |
364 val t = TermC.typ_a2real (Syntax.read_term_global thy str); |
365 val t = Model_Pattern.adapt_term_to_type ctxt (Syntax.read_term_global thy str); |
365 Thm.global_cterm_of thy t; |
366 Thm.global_cterm_of thy t; |
366 case TermC.parseNEW ctxt str of |
367 case TermC.parseNEW ctxt str of |
367 SOME t' => t' |
368 SOME t' => t' |
368 | NONE => error "termC.sml parsing 'x + 2*z' failed"; |
369 | NONE => error "termC.sml parsing 'x + 2*z' failed"; |
369 |
370 |
447 val ctxt = Proof_Context.init_global thy; |
448 val ctxt = Proof_Context.init_global thy; |
448 val ctxt = Config.put show_types true ctxt; |
449 val ctxt = Config.put show_types true ctxt; |
449 "----- read_term_pattern ---"; |
450 "----- read_term_pattern ---"; |
450 val t = (thy, str) |>> Proof_Context.init_global |
451 val t = (thy, str) |>> Proof_Context.init_global |
451 |-> Proof_Context.read_term_pattern; |
452 |-> Proof_Context.read_term_pattern; |
452 val t_real = TermC.typ_a2real t; |
453 val t_real = Model_Pattern.adapt_term_to_type ctxt t; |
453 if UnparseC.term_in_ctxt ctxt t_real = |
454 if UnparseC.term_in_ctxt ctxt t_real = |
454 "\<not> (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) \<or>\n " |
455 "\<not> (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) \<or>\n " |
455 ^ "matchsub (?a + (?b - ?c)) t_t \<or>\n " |
456 ^ "matchsub (?a + (?b - ?c)) t_t \<or>\n " |
456 ^ "matchsub (?a - (?b + ?c)) t_t \<or> matchsub (?a + (?b - ?c)) t_t)" then () |
457 ^ "matchsub (?a - (?b + ?c)) t_t \<or> matchsub (?a + (?b - ?c)) t_t)" then () |
457 else error "matchsub"; |
458 else error "matchsub"; |