77 (thy, tac_, (is, ctxt''), (pp, Res), pt); |
77 (thy, tac_, (is, ctxt''), (pp, Res), pt); |
78 val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete; |
78 val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete; |
81 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR","uval (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *); |
81 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR","uval (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *); |
82 if nxt = ("Check_Postcond", Check_Postcond ["LINEAR", "univariate", "equation", "test"]) |
82 case nxt of ("Check_Postcond", Check_Postcond ["LINEAR", "univariate", "equation", "test"]) => () |