Lines Matching refs:SPEC
205 (* representation in ARM SPEC *)
247 (* representation in M0 SPEC *)
357 | ARM arm_c => SPEC ARM_MODEL (arm_STATE s * arm_PC n) arm_c
359 | M0 m0_c => SPEC M0_MODEL (m0_STATE s * m0_PC n) m0_c
1297 ``SPEC ARM_MODEL (arm_assert_for ((NextNode i,st,name)::t)) code
1301 ``SPEC M0_MODEL (m0_assert_for ((NextNode i,st,name)::t)) code
1341 SPEC ^model_tm (^assert_for_tm s1) code (^assert_for_tm s2)``,
1581 \\ ASSUME_TAC (DIVISION |> Q.SPEC `2` |> SIMP_RULE std_ss []
1582 |> GSYM |> Q.SPEC `n`)
1598 \\ ASSUME_TAC (DIVISION |> Q.SPEC `4` |> SIMP_RULE std_ss [] |> GSYM |> Q.SPEC `n`)
1634 SPEC ARM_MODEL (arm_PC p * cond (SKIP_TAG asm)) {} (arm_PC (p + 4w))``,
1638 ``SPEC ARM_MODEL (aPC p * aR 0w r0 * cond (unspecified_pre)) {}
1660 \\ MP_TAC (MATCH_MP DIVISION (DECIDE ``0<4:num``) |> Q.SPEC `n'`)
1970 ``SPEC m (p * f x) c (q * f x) <=>
1971 !v. (v = x) ==> SPEC m (p * f v) c (q * f v)``,
1975 ``(b1 ==> SPEC m p c1 q1) /\ (b2 ==> SPEC m p c2 q2) ==>
1976 (~b1 ==> b2) ==> SPEC m p (c1 UNION c2) (if b1 then q1 else q2)``,
1984 ``SPEC m (p * r x) c q ==>
1985 !pc. (pc = x) ==> SPEC m (p * r pc) c q``,
1990 (a ==> SPEC x p c q) ==> !d. c SUBSET d ==> a ==> SPEC x p d q``,