27 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
27 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
28 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
28 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
29 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
29 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
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; |
31 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
32 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; (*OKnxt = Apply_Method ["Test", "solve_linear"]*) |
33 val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set_Inst isolate_bdv*); |
33 val (p'',_,f,nxt,_,pt'') = me nxt p [] pt; (*nxt = Rewrite_Set_Inst..OK isolate_bdv*); |
34 get_ctxt pt p |> is_e_ctxt; (*false*) |
34 get_ctxt pt'' p'' |> is_e_ctxt; (*OKfalse*) |
35 val ctxt = get_ctxt pt p; |
35 val ctxt = get_ctxt pt'' p''; |
36 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; |
36 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; |
37 get_loc pt p |> snd |> is_e_ctxt; (*false*) |
37 get_loc pt'' p'' |> snd |> is_e_ctxt; (**OKfalse*) |
38 |
38 |
39 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*); |
39 val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set "Test_simplify"*); |
40 get_ctxt pt p |> is_e_ctxt; (*false*) |
40 get_ctxt pt p |> is_e_ctxt; (*false*) |
41 val ctxt = get_ctxt pt p; |
41 val ctxt = get_ctxt pt p; |
42 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; |
42 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; |
43 get_loc pt p |> snd |> is_e_ctxt; (*false*) |
43 get_loc pt p |> snd |> is_e_ctxt; (*false*) |
44 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *); |
44 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *); |
82 (set as Const ("Set.Collect",_) $ Abs (_,_,pred)))) = (pt, (assoc_thy th), stac); |
82 (set as Const ("Set.Collect",_) $ Abs (_,_,pred)))) = (pt, (assoc_thy th), stac); |
83 (*2011 changed ^^^^^ *) |
83 (*2011 changed ^^^^^ *) |
84 |
84 |
85 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*) |
85 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*) |
86 if nxt = ("Check_elementwise", Check_elementwise "Assumptions") then () |
86 if nxt = ("Check_elementwise", Check_elementwise "Assumptions") then () |
87 else error "Check_elementwise changed; after switch sub-->root-method" |
87 else error "Check_elementwise changed; after switch sub-->root-method"; |