equal
deleted
inserted
replaced
111 > val pt = union_asm pt p |
111 > val pt = union_asm pt p |
112 [("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]), |
112 [("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]), |
113 ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])]; |
113 ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])]; |
114 > val p = []; |
114 > val p = []; |
115 > val (sss,ttt) = mk_set thy pt p consts pred; |
115 > val (sss,ttt) = mk_set thy pt p consts pred; |
116 > (Syntax.string_of_term (thy2ctxt thy) sss,Sign.string_of_term(sign_of thy) ttt); |
116 > (Syntax.string_of_term (thy2ctxt thy) sss,Syntax.string_of_term(thy2ctxt thy) ttt); |
117 val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ... |
117 val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ... |
118 |
118 |
119 val consts = str2term "UniversalList"; |
119 val consts = str2term "UniversalList"; |
120 val pred = str2term "Assumptions"; |
120 val pred = str2term "Assumptions"; |
121 |
121 |