equal
deleted
inserted
replaced
292 else (); |
292 else (); |
293 "--- 15<> ---"; |
293 "--- 15<> ---"; |
294 (* val nxt = ("End_Proof'",End_Proof');*) |
294 (* val nxt = ("End_Proof'",End_Proof');*) |
295 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
295 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
296 |
296 |
297 writeln (pr_ptree pr_short pt); |
297 writeln (pr_ctree pr_short pt); |
298 writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^ |
298 writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^ |
299 "\n============================================================="); |
299 "\n============================================================="); |
300 (*get_obj g_asm pt []; |
300 (*get_obj g_asm pt []; |
301 val it = [("#0 <= sqrt x + sqrt (#5 + x)",[1]),("#0 <= #9 + #4 * x",[1]),...*) |
301 val it = [("#0 <= sqrt x + sqrt (#5 + x)",[1]),("#0 <= #9 + #4 * x",[1]),...*) |
302 |
302 |