Searched refs:rw (Results 151 - 175 of 182) sorted by relevance

12345678

/seL4-l4v-10.1.1/HOL4/src/integer/
H A Dint_bitwiseScript.sml128 \\ rw [MOD_TIMES,MOD_EQ_0]);
/seL4-l4v-10.1.1/HOL4/src/n-bit/
H A DalignmentScript.sml234 \\ rw [aligned_extract, align_sub, wordsTheory.WORD_EXTRACT_COMP_THM,
H A DwordsLib.sml2469 val rw = [word_0, word_T, word_L, word_xor_def, word_or_def, word_and_def, value
2524 [fcpLib.FCP_ss, SIZES_ss, simpLib.rewrites rw,
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/arm/
H A Dprog_armLib.sml175 val rw = (INST (fst (match_term fff x)) o SPEC_ALL o GSYM) aBYTE_MEMORY_INSERT value
176 val th = DISCH ((fst o dest_imp o concl) rw) th
261 val rw = (INST (fst (match_term fff x)) o SPEC_ALL) aMEMORY_INSERT value
262 val th = DISCH ((fst o dest_imp o concl) rw) th
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A Dselftest.sml441 val rw = pvRw (eqnsToRw eqns); value
442 val th = pvThm (snd (try (Rewrite.rewriteConv rw kboCmp) (T`e * e`)));
443 val th = pvThm (snd (try (Rewrite.rewriteConv rw kboCmp) (T`e * (i $z * $z)`)));
444 val th = pvThm (try (Rewrite.rewriteRule rw kboCmp) ax);
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A Dselftest.sml441 val rw = pvRw (eqnsToRw eqns); value
442 val th = pvThm (snd (try (Rewrite.rewriteConv rw kboCmp) (T`e * e`)));
443 val th = pvThm (snd (try (Rewrite.rewriteConv rw kboCmp) (T`e * (i $z * $z)`)));
444 val th = pvThm (try (Rewrite.rewriteRule rw kboCmp) ax);
/seL4-l4v-10.1.1/seL4/manual/parts/
H A Dapi.tex93 '\texttt{seL4\_Word rw}', the access direction that will currently trigger the breakpoint,
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibClauseset.sml553 val rw = value
558 sp o olist o sb o strengthen s o rw
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A Dgraph_specsLib.sml193 val rw = RAND_CONV (fn tm => ASSUME assum) tm value
194 val th = RW1 [rw] th
H A DGraphLangScript.sml1810 \\ rw []
1825 \\ rw []
1836 val rw = prove( value
1923 |> CONJ rw |> CONJ rw3 |> CONJ rw64 |> CONJ rw16 |> CONJ rw8 |> CONJ rw4
/seL4-l4v-10.1.1/HOL4/examples/unification/triangular/nominal/
H A DntermScript.sml253 simp[nterm_case_rewrites, Sus_case1] >> eq_tac >> rw[]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A DregAllocation.sml879 val rw = (RewrBody (mk_mem_rules (Type `:num`))) o (RewrBody (mk_mem_rules (Type `:word32`))) o value
898 else rw exp
907 val newDecl = mk_comb (f, rw args)
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A DregAllocation.sml879 val rw = (RewrBody (mk_mem_rules (Type `:num`))) o (RewrBody (mk_mem_rules (Type `:word32`))) o value
898 else rw exp
907 val newDecl = mk_comb (f, rw args)
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A DregAllocation.sml879 val rw = (RewrBody (mk_mem_rules (Type `:num`))) o (RewrBody (mk_mem_rules (Type `:word32`))) o value
898 else rw exp
907 val newDecl = mk_comb (f, rw args)
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/
H A Dlisp_opsScript.sml1266 fun ARM_LISP_EQ_SYMBOL (i,name,rw) (j,str) = let
1285 val result = RW [GSYM rw] result
1288 fun X86_LISP_EQ_SYMBOL (i,name,rw) (j,str) = let
1311 val result = RW [GSYM rw] result
1314 fun PPC_LISP_EQ_SYMBOL (i,name,rw) (j,str) = let
1335 val result = RW [GSYM rw] result
H A Dlisp_finalScript.sml501 val rw = RW [] (MATCH_MP SET_TO_LIST_THM FINITE_EMPTY) value
504 val thi = SIMP_RULE std_ss [rw,fmap2list_def,FDOM_FEMPTY,MAP,alist2sexp_def,list2sexp_def,LISP_EVAL_def] thi
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/lambek/
H A DExampleScript.sml476 >> rw [MAX_EQ_0]);
/seL4-l4v-10.1.1/HOL4/src/floating-point/
H A Dmachine_ieeeLib.sml308 rw [float_to_fp_def, fp_to_float_def,
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/
H A DcoreScript.sml664 PCCHANGE rwa = let (rw,a:word4) = rwa in rw /\ (a = 15w)`;
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/step/
H A Darm_stepLib.sml250 val rwt = Q.prove (`!b. ((if b then 16 else 32) = 16n) = b`, rw [])
618 rw [] \\ wordsLib.n2w_INTRO_TAC 5 \\ blastLib.BBLAST_TAC
641 rw [])
985 rw [])
4031 rw [GoodMode_def]
4056 rw [] \\ fs [] \\ blastLib.BBLAST_TAC)
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/
H A Dvars_as_resourceFunctor.sml4020 | gen_step_tac_opt_eval (p, (rw, cv, ss))
4022 gen_step_tac_opt_eval (p, (rw@thmL, cv, ss)) gstoL
4023 | gen_step_tac_opt_eval (p, (rw, cv, ss))
4025 gen_step_tac_opt_eval (p, (rw, cv@convL, ss)) gstoL
4026 | gen_step_tac_opt_eval (p, (rw, cv, ss))
4028 gen_step_tac_opt_eval (p, (rw, cv, ss@ssfL)) gstoL
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/step/
H A Dm0_stepLib.sml1472 val rw = REWRITE_CONV (gen_rws "decode Thumb" rwts_16 @ value
1484 (rw tm
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/
H A Dmilawa_proofpScript.sml14 val rw = ref (tl [TRUTH]); value
16 fun add_rw th = (rw := th::(!rw); th);
17 fun add_rws thms = (rw := thms @ (!rw));
33 fun SS thms = SIMP_TAC std_ss (thms @ !rw)
34 fun FS thms = FULL_SIMP_TAC std_ss (thms @ !rw)
35 fun SR thms = SIMP_RULE std_ss (thms @ !rw)
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/step/
H A Dx64_stepLib.sml812 strip_tac \\ Cases \\ rw [])
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DksTools.sml382 val _ = with_flag (show_types,true) (DMSG (TM (concl res))) dbgkt val _ = DMSG (ST "rw term") dbgkt

Completed in 388 milliseconds

12345678