/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | int_bitwiseScript.sml | 128 \\ rw [MOD_TIMES,MOD_EQ_0]);
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | alignmentScript.sml | 234 \\ rw [aligned_extract, align_sub, wordsTheory.WORD_EXTRACT_COMP_THM,
|
H A D | wordsLib.sml | 2469 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 D | prog_armLib.sml | 175 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 D | selftest.sml | 441 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 D | selftest.sml | 441 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 D | api.tex | 93 '\texttt{seL4\_Word rw}', the access direction that will currently trigger the breakpoint,
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibClauseset.sml | 553 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 D | graph_specsLib.sml | 193 val rw = RAND_CONV (fn tm => ASSUME assum) tm value 194 val th = RW1 [rw] th
|
H A D | GraphLangScript.sml | 1810 \\ 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 D | ntermScript.sml | 253 simp[nterm_case_rewrites, Sus_case1] >> eq_tac >> rw[]
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | regAllocation.sml | 879 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 D | regAllocation.sml | 879 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 D | regAllocation.sml | 879 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 D | lisp_opsScript.sml | 1266 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 D | lisp_finalScript.sml | 501 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 D | ExampleScript.sml | 476 >> rw [MAX_EQ_0]);
|
/seL4-l4v-10.1.1/HOL4/src/floating-point/ |
H A D | machine_ieeeLib.sml | 308 rw [float_to_fp_def, fp_to_float_def,
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/ |
H A D | coreScript.sml | 664 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 D | arm_stepLib.sml | 250 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 D | vars_as_resourceFunctor.sml | 4020 | 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 D | m0_stepLib.sml | 1472 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 D | milawa_proofpScript.sml | 14 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 D | x64_stepLib.sml | 812 strip_tac \\ Cases \\ rw [])
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | ksTools.sml | 382 val _ = with_flag (show_types,true) (DMSG (TM (concl res))) dbgkt val _ = DMSG (ST "rw term") dbgkt
|