105 then [pred] |
105 then [pred] |
106 else (map fst) (get_assumptions_ pt (p,Res)) |
106 else (map fst) (get_assumptions_ pt (p,Res)) |
107 in (bdv, pred) end |
107 in (bdv, pred) end |
108 |
108 |
109 | mk_set thy _ _ l _ = |
109 | mk_set thy _ _ l _ = |
110 error ("check_elementwise: no set "^ |
110 error ("check_elementwise: no set " ^ term2str l); |
111 (Syntax.string_of_term (thy2ctxt thy) l)); |
|
112 (*> val consts = str2term "[x=#4]"; |
111 (*> val consts = str2term "[x=#4]"; |
113 > val pred = str2term "Assumptions"; |
112 > val pred = str2term "Assumptions"; |
114 > val pt = union_asm pt p |
113 > val pt = union_asm pt p |
115 [("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]), |
114 [("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]), |
116 ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])]; |
115 ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])]; |
117 > val p = []; |
116 > val p = []; |
118 > val (sss,ttt) = mk_set thy pt p consts pred; |
117 > val (sss,ttt) = mk_set thy pt p consts pred; |
119 > (Syntax.string_of_term (thy2ctxt thy) sss,Syntax.string_of_term(thy2ctxt thy) ttt); |
118 > (term2str sss, term2str ttt); |
120 val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ... |
119 val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ... |
121 |
120 |
122 val consts = str2term "UniversalList"; |
121 val consts = str2term "UniversalList"; |
123 val pred = str2term "Assumptions"; |
122 val pred = str2term "Assumptions"; |
124 |
123 |