Lines Matching defs:msr
96 val msr = MP (CONV_RULE lzFORALL_IMP_CONV (ISPECL [state,ksname] MU_SAT_RV)) wfKS_ks
99 in (msr,mk_seths mf,msreq) end
183 fun mk_rv_spec_thm msr seth sel msreq ie ee state (tb,gth,sth,env,ix,rsc,ithm,abthm,_,_) dp mf =
190 (*val _ = dbgTools.DTH (dpfx^ msr) val _ = dbgTools.DST (dpfx^ "msr\n") (*DBG*)
204 val _ = dbgTools.DTH (dpfx^ (ISPECL [ie,fromMLstring v] msr))
212 (ISPECL [ie,bv] msr)) end
399 | muCheck_aux ((_,_,(msr,_,msreq,ee),_,_),(seth,sel,state,ie)) mf vm dp (muRV cch) =
401 val tb = cache_get cch ie (mk_rv_tb ee (!cch)) (mk_rv_spec_thm msr seth sel msreq ie ee state (!cch) dp) dp []
760 val (msr,(seth,sel),msreq) = mk_gen_rv_thms mf ksname state rvl ie wfKS_ks
786 in (ie,(msr,seth,sel,msreq,ee2),mfml,imf_thms,frv_thms,qd,sqd,mf) end
804 val (ie,(msr,seth,sel,msreq,ee2),mfml,imf_thms,frv_thms,qd,sqd,mf) =
815 (msr,seth,msreq,ee2),