30 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
30 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
31 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*) |
31 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*) |
32 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*); |
32 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*); |
33 case nxt of (Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")) => () |
33 case nxt of (Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")) => () |
34 | _ => error "Rewrite_Set_Inst changed"; |
34 | _ => error "Rewrite_Set_Inst changed"; |
|
35 |
|
36 (*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*) |