Searched refs:rw (Results 176 - 182 of 182) sorted by relevance
12345678
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/step/ |
| H A D | mips_stepLib.sml | 37 rw []
|
| /seL4-l4v-10.1.1/HOL4/src/n-bit/ |
| H A D | wordsScript.sml | 1047 rw [w2n_minus1, DECIDE ``0n < a ==> (a - 1 + 1 = a)``]
3268 \\ rw [word_lsl_n2w, MULT_DIV, ZERO_DIV]
4658 \\ rw [sum_numTheory.SUM_def]
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/src/ |
| H A D | riscv.spec | 872 bool check_CSR_access(rw::csrRW, pr::csrPR, p::Privilege, a::accessType) =
873 (a == Read or rw != 0b11) and (privLevel(p) >=+ pr)
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/ |
| H A D | lisp_gcScript.sml | 2492 fun prove_eq n1 n2 rw goal = prove(goal,
2493 STRIP_TAC \\ TAILREC_TAC \\ SIMP_TAC std_ss ([LET_DEF,word_arith_lemma1] @ rw)
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | integerScript.sml | 2391 rw[INT_ABS, EQ_IMP_THM] >>
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/model/ |
| H A D | riscv.sml | 2365 fun check_CSR_access (rw,(pr,(p,a))) =
2366 ((a = Read) orelse (not(rw = (BitsN.B(0x3,2))))) andalso
|
| H A D | riscvScript.sml | 1633 TP[Var("rw",FTy 2),Var("pr",FTy 2),Var("p",CTy"Privilege"),
1637 Mop(Not,EQ(Var("rw",FTy 2),LW(3,2)))),
|
Completed in 238 milliseconds
12345678