| /seL4-l4v-master/HOL4/polyml/ |
| H A D | install-sh | 393 prefixes=
401 prefixes=
413 prefixes="$prefixes '$qprefix'"
419 if test -n "$prefixes"; then
422 eval "\$doit_exec \$mkdirprog $prefixes") ||
|
| /seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
| H A D | x64_astScript.sml | 70 (* This semantics understands the following prefixes in addition to the REX prefix. *)
|
| H A D | x64_decoderScript.sml | 22 the instruction, i.e. after all the other prefixes.
633 (* find pre-evaulatable prefixes *)
643 val prefixes = thZ |> concl |> dest_eq |> snd |> cdr |> rec_dest_DTF value
644 (* evaluate the prefixes *)
651 val pre_evaluated_thm = LIST_CONJ (map eval_for prefixes)
|
| H A D | x64_encodeLib.sml | 212 val prefixes = if zsize = 16 then "66" else "" value
291 val e = prefixes ^ (rex_prefix()) ^ e
|
| H A D | x64_opsemScript.sml | 429 x64_execute ii (Zfull_inst prefixes i) len =
430 if MEM Zlock prefixes then lockT (x64_exec ii i len) else x64_exec ii i len`;
|
| /seL4-l4v-master/HOL4/src/AI/sml_inspection/ |
| H A D | smlPrettify.sml | 56 Removing structure prefixes. Also prefers lower case if available.
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/x64/model/ |
| H A D | x64.sml | 3039 val prefixes = Set.mk p value
3040 val op_size_override = Set.mem(BitsN.B(0x66,8),prefixes)
3042 if Set.mem(BitsN.B(0x67,8),prefixes)
4377 val (prefixes,v) = e_opsize(sz,rex) value
4385 then Option.SOME(prefixes,(v,l))
4392 then Option.SOME(prefixes,(v,l))
4399 then Option.SOME(prefixes,(v,l))
4403 then Option.SOME(prefixes,(v,e_imm64 imm))
4417 val (prefixes,v) = e_opsize(sz,rex) value
4420 List.concat[prefixes,
4437 val (prefixes,v) = e_opsize(sz,rex) value
4448 val prefixes = L3.fst(e_opsize(sz,rex)) value
5310 val (prefixes,v) = e_opsize(sz,rex) value
[all...] |
| H A D | x64Script.sml | 6099 Let(Var("prefixes",STy F8),Mop(SofL,Var("p",LTy F8)),
6101 Bop(In,LW(102,8),Var("prefixes",STy F8)),
6102 ITE(Bop(In,LW(103,8),Var("prefixes",STy F8)),
10236 Let(TP[Var("prefixes",LTy F8),Var("v",F8)],
10248 TP[Var("prefixes",LTy F8),Var("v",F8),
10257 TP[Var("prefixes",LTy F8),Var("v",F8),
10266 TP[Var("prefixes",LTy F8),Var("v",F8),
10272 TP[Var("prefixes",LTy F8),Var("v",F8),
10294 Let(TP[Var("prefixes",LTy F8),Var("v",F8)],
10298 CC[Var("prefixes",LT
[all...] |
| /seL4-l4v-master/HOL4/examples/HolCheck/ |
| H A D | profTools.sml | 131 fun prapl l = if !prf then (List.app sp l;prat()) else () (* print only the ones with prefixes in l *)
|
| /seL4-l4v-master/isabelle/src/Pure/Admin/ |
| H A D | build_log.scala | 134 prefixes: List[String] =
141 prefixes.exists(name.startsWith(_)) &&
|
| /seL4-l4v-master/l4v/isabelle/src/Pure/Admin/ |
| H A D | build_log.scala | 134 prefixes: List[String] =
141 prefixes.exists(name.startsWith(_)) &&
|
| /seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
| H A D | EXPORT_PARSETREE.sml | 156 simple prefixes. *)
|
| /seL4-l4v-master/HOL4/src/pred_set/src/ |
| H A D | set_relationScript.sml | 1703 (* A big theorem that a partial order with finite prefixes over a countable*)
1704 (* set can be extended to a linear order with finite prefixes. *)
|
| /seL4-l4v-master/HOL4/examples/PSL/1.01/executable-semantics/ |
| H A D | ExecuteSemanticsScript.sml | 1150 has a bad prefix [] for the property, but there are no bad prefixes for
|
| /seL4-l4v-master/HOL4/src/parse/ |
| H A D | parse_term.sml | 357 for all x on right hand side of prefixes and infixes below
|
| /seL4-l4v-master/HOL4/examples/PSL/1.1/executable-semantics/ |
| H A D | ExecuteSemanticsScript.sml | 1335 has a bad prefix [] for the property, but there are no bad prefixes for
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/arm/step/ |
| H A D | arm_stepLib.sml | 2473 val prefixes = List.rev (mlibUseful.sort_map String.size Int.compare value
2492 else List.find (fn p => String.isPrefix p a) prefixes
|
| /seL4-l4v-master/isabelle/src/Doc/Intro/document/ |
| H A D | foundations.tex | 734 Here, lifting prefixes an object-rule's premises and conclusion with $\Forall
|
| /seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/ |
| H A D | foundations.tex | 734 Here, lifting prefixes an object-rule's premises and conclusion with $\Forall
|
| /seL4-l4v-master/l4v/isabelle/src/Doc/Sledgehammer/document/ |
| H A D | root.tex | 936 simultaneously. The files are identified by the prefixes \texttt{prob\_} and
|
| /seL4-l4v-master/isabelle/src/Doc/Sledgehammer/document/ |
| H A D | root.tex | 936 simultaneously. The files are identified by the prefixes \texttt{prob\_} and
|
| /seL4-l4v-master/l4v/isabelle/src/Doc/Nitpick/document/ |
| H A D | root.tex | 1070 prefixes of length $K$. However, setting $K$ to a too low value can
|
| /seL4-l4v-master/isabelle/src/Doc/Nitpick/document/ |
| H A D | root.tex | 1070 prefixes of length $K$. However, setting $K$ to a too low value can
|
| /seL4-l4v-master/HOL4/src/coalgebras/ |
| H A D | llistScript.sml | 599 (* can also prove llist equality by proving all prefixes are the same *)
|