45 2.ERROR WAS: *** stac2tac_ TODO: no match for (Rewrite_Set ''norm_equation'') (x + 1 = 2)*) |
45 2.ERROR WAS: *** stac2tac_ TODO: no match for (Rewrite_Set ''norm_equation'') (x + 1 = 2)*) |
46 "~~~~~ we continue with (@2) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~"; |
46 "~~~~~ we continue with (@2) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~"; |
47 "~~~~~ fun me, args:"; val tac = nxt; |
47 "~~~~~ fun me, args:"; val tac = nxt; |
48 val ("ok", (_, _, (pt''''',p'''''))) = locatetac tac (pt,p); |
48 val ("ok", (_, _, (pt''''',p'''''))) = locatetac tac (pt,p); |
49 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p); |
49 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p); |
50 val (mI,m) = mk_tac'_ tac; (*mI = "Apply_Method"*) |
|
51 val Appl m = applicable_in p pt m; (*m = Apply_Method'..*) |
50 val Appl m = applicable_in p pt m; (*m = Apply_Method'..*) |
52 member op = specsteps mI; (*false*) |
51 member op = specsteps mI; (*false*) |
53 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = (m, ptp); |
52 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = (m, ptp); |
54 "~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,_), pos as (p,_)) = (m, pos); |
53 "~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,_), pos as (p,_)) = (m, pos); |
55 val PblObj {meth, ctxt, ...} = get_obj I pt p; |
54 val PblObj {meth, ctxt, ...} = get_obj I pt p; |