| /seL4-l4v-master/HOL4/examples/ARM/v7/eval/ |
| H A D | emit_eval.sml | 349 | armML.Miscellaneous (armML.Swap _) => "swap"
|
| /seL4-l4v-master/HOL4/examples/Crypto/TWOFISH/ |
| H A D | twofishScript.sml | 509 Finally the output whitening step undoes the `swap' of the
|
| /seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
| H A D | Useful.sml | 105 fun swap (x,y) = (y,x); function
|
| /seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Useful.sml | 105 fun swap (x,y) = (y,x); function
|
| /seL4-l4v-master/HOL4/src/portableML/ |
| H A D | Portable.sml | 72 fun swap (x, y) = (y, x) function
|
| /seL4-l4v-master/HOL4/src/1/ |
| H A D | boolSyntax.sml | 569 fun list_mk_ucomb (f, args) = List.foldl (mk_ucomb o swap) f args
|
| H A D | Drule.sml | 607 val t = (mk_eq o Lib.swap o dest_eq o dest_neg o concl) th
2337 val swap = IMP_ANTISYM_RULE (DISCH eq imp1) (DISCH ex imp2) value
2339 GEN Bvar (TRANS (SPEC Bvar th2) swap)
|
| H A D | Conv.sml | 1753 * SWAP_EXISTS_CONV: swap the order of existentially quantified vars. *
1836 * SWAP_FORALL_CONV: swap the order of existentially quantified vars. *
|
| /seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/binomial/ |
| H A D | binomial.tex | 329 \verb@REWRITE_TAC@ to swap the terms \verb@a@ and \verb@b@.
366 Now the equation \verb@eqn@ can be used to prove swap terms
|
| /seL4-l4v-master/HOL4/Manual/Tutorial/binomial/ |
| H A D | binomial.tex | 329 \verb@REWRITE_TAC@ to swap the terms \verb@a@ and \verb@b@.
366 Now the equation \verb@eqn@ can be used to prove swap terms
|
| /seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
| H A D | lisp_invScript.sml | 164 (* swap *)
210 (* e.g. to swap 4 and 5 do generate_swap 4 5 *)
|
| /seL4-l4v-master/HOL4/src/n-bit/ |
| H A D | wordsLib.sml | 436 (Lib.swap ## Lib.swap)
1818 else (Lib.swap o fcpSyntax.dest_fcp_index, wordsTheory.word_bit)
|
| /seL4-l4v-master/isabelle/src/Doc/Logics/document/ |
| H A D | LK.tex | 634 elimination rules, and of course there is no swap rule. As always,
|
| /seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/ |
| H A D | LK.tex | 634 elimination rules, and of course there is no swap rule. As always,
|
| /seL4-l4v-master/HOL4/examples/ARM_security_properties/ |
| H A D | user_lemma_instructionsScript.sml | 784 (* swap *)
|
| /seL4-l4v-master/HOL4/examples/algebra/group/ |
| H A D | groupScript.sml | 724 (* Theorem: [Inverse equality swap]: |/x = y <=> x = |/y *)
|
| /seL4-l4v-master/HOL4/src/HolSmt/ |
| H A D | Z3_ProofReplay.sml | 402 val tm' = boolSyntax.mk_eq (Lib.swap (boolSyntax.dest_eq tm))
|
| /seL4-l4v-master/HOL4/src/list/src/ |
| H A D | ListConv1.sml | 30 (* Minor tweak to EL_CONV to take account of swap in quantifiers in defn *)
|
| /seL4-l4v-master/HOL4/examples/HolCheck/ |
| H A D | lzConv.sml | 1526 (* SWAP_EXISTS_CONV: swap the order of existentially quantified vars. *)
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
| H A D | stateLib.sml | 1069 val df_intro = List.foldl (pred_setSyntax.mk_delete o Lib.swap) df
|
| /seL4-l4v-master/HOL4/examples/AKS/compute/ |
| H A D | computeBasicScript.sml | 1621 if (n > m) swap (n, m) // ensure n <= m
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/arm/model/ |
| H A D | arm.sml | 24090 fun p_smuad_smusd (c,(sub,(swap,l))) =
24095 (SignedMultiplyDual(sub,(swap,(rd,(rn,(rm,BitsN.B(0xF,4))))))))
24098 fun p_smlad_smlsd (c,(sub,(swap,l))) =
24101 OK(c,Multiply(SignedMultiplyDual(sub,(swap,(rd,(rn,(rm,ra)))))))
24104 fun p_smlald_smlsld (c,(sub,(swap,l))) =
24109 (SignedMultiplyLongDual(sub,(swap,(rdhi,(rdlo,(rn,rm)))))))
|
| /seL4-l4v-master/HOL4/examples/ARM/v7/ |
| H A D | arm_opsemScript.sml | 2853 instruction ii "swap" ALL
|
| H A D | arm_parserLib.sml | 1241 | _ => raise ERR "swap_opcode" "cannot swap opcode";
|
| /seL4-l4v-master/HOL4/examples/ARM_security_properties/model/ |
| H A D | arm_opsemScript.sml | 2877 instruction ii "swap" ALL
|