Lines Matching refs:var
285 | var 'a
348 (CCS_Subst (var Y) E' X = if (Y = X) then E' else (var Y)) /\
363 (* |- ���X E. CCS_Subst (var X) E X = E (2nd fixed point of CCS_Subst) *)
366 (REWRITE_CONV [CCS_Subst_def] ``CCS_Subst (var X) E X``));
451 |- !X u E'. ~TRANS (var X) u E'
456 (Q.SPECL [`var X`, `u`, `E`] TRANS_cases)));
828 (FV (var X) = {X}) /\
839 (BV (var X) = EMPTY) /\
859 (CCS_Subst1 (var Y) fm = if (Y IN FDOM fm) then (FAPPLY fm Y)
860 else (var Y)) /\
956 (FN (var X) J = EMPTY) /\
969 (BN (var X) J = EMPTY) /\