equal
deleted
inserted
replaced
219 val pos = lev_on pos; |
219 val pos = lev_on pos; |
220 (*val pos = ([4,1,2]+) *) |
220 (*val pos = ([4,1,2]+) *) |
221 val (pt,_) = cappend_parent(*pbl*) pt pos loc "f_y = d/dy x \<up> 3 ..." |
221 val (pt,_) = cappend_parent(*pbl*) pt pos loc "f_y = d/dy x \<up> 3 ..." |
222 Empty_Tac TransitiveB; |
222 Empty_Tac TransitiveB; |
223 "--- 4 ---"; |
223 "--- 4 ---"; |
224 writeln (pr_ctree pr_short pt); |
224 writeln (pr_ctree ctxt pr_short pt); |
225 |
225 |
226 (* |
226 (* |
227 . ----- pblobj ----- |
227 . ----- pblobj ----- |
228 1. {(a,b). is-max ... |
228 1. {(a,b). is-max ... |
229 1.1. {(a,b). is-max ... |
229 1.1. {(a,b). is-max ... |