/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 646 the integer type \textit{my\_int} by encoding the integer $x$ by a pair of 677 that converts the pair notation to the standard mathematical notation: 1974 is approximated by a subset of the possible function or pair values. 2626 unregistering postprocessors consists of the following pair of functions defined 2650 pair of functions defined in the \textit{Nitpick\_HOL} structure:
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Drule.sml | 2407 * Take an AC pair, normalize them, then prove left-commutativity * 2420 (* Classify a pair of theorems as one assoc. thm and one comm. thm. Then 2421 return pair (A,C) where A has the form |- f(x,f(y,z)) = f(f(x,y),z) *)
|
H A D | Pmatch.sml | 617 val constrs_type = map (pair (type_of arg)) constrs
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | wordsLib.sml | 493 |> List.map (fn (thy, l) => List.map (Lib.pair thy) l) 499 (s, map (pair "words") 504 map (pair "arithmetic")
|
/seL4-l4v-10.1.1/HOL4/Manual/Description/ |
H A D | HolBdd.tex | 655 The integer returned as the first component of the pair is a pointer 960 A finalized value, in the \mosml{} runtime system, is a pair where the 2258 A state of the iteration is a pair (tb,tb') consisting of the
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | HolBdd.tex | 655 The integer returned as the first component of the pair is a pointer 960 A finalized value, in the \mosml{} runtime system, is a pair where the 2258 A state of the iteration is a pair (tb,tb') consisting of the
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/model/ |
H A D | arm8.sml | 2451 (acctype,(excl,(pair,(rn_unknown,(rt_unknown,(s,(n,(t,t2)))))))))) = 2452 if pair 2478 (size,(memop,(acctype,(excl,(pair,(Rs,(Rn,(Rt,Rt2)))))))) = 2481 if (memop = MemOp_LOAD) andalso (pair andalso (Rt = Rt2)) 2489 (pair andalso (Rs = Rt2)) 2521 (excl,(pair,(rn_unknown,(rt_unknown,(Rs,(Rn,(Rt,Rt2)))))))))) 5360 val pair = (BitsN.fromBitstring([o1'0],1)) = (BitsN.B(0x1,1)) value 5367 (pair,
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_OPTIMISER.sml | 860 (* Return the pair of functions. *) 1048 an argument is a function with tupled or curried arguments into a pair
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | Import.sml | 118 ParseDatatype.dTyop {Thy = SOME "pair", Tyop = "prod", Args = [t1, t2]}
|
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
H A D | ConsThms.sml | 442 a pair consisting of the definition of the function and the name of
|
/seL4-l4v-10.1.1/HOL4/src/meson/src/ |
H A D | mesonLib.sml | 549 then failwith "repetition of demigoal pair"
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | folMapping.sml | 144 val new_var = fake_new_var o (new_string ## I) o pair ();
|
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | CCSScript.sml | 224 (SND of any pair is a name, FST can be either name or coname)
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
H A D | DerivedBddRules.sml | 637 (* A state of the iteration is a pair (tb,tb') consisting of the *)
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | ksTools.sml | 136 T is a (string * term) list where each pair is (action name, corresponding transition relation)
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
H A D | DEBUGGER_.sml | 230 During compilation the environment is built up as a pair
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/ |
H A D | LK.tex | 574 A \textbf{pack} is a pair whose first component is a list of safe rules and
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/ |
H A D | LK.tex | 574 A \textbf{pack} is a pair whose first component is a list of safe rules and
|
/seL4-l4v-10.1.1/HOL4/examples/dev/ |
H A D | compile.sml | 446 (* Rec or Let. If so return a pair (constructor, args), else return (tm,[]) *) 1238 (* returns a pair consisting of a list of existentially quantified vars *)
|
/seL4-l4v-10.1.1/HOL4/src/pred_set/Manual/ |
H A D | description.tex | 591 with four elements (each a number), two elements (each of which is a pair), and 592 one element (a pair of pairs) respectively.
|
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/ |
H A D | alphaScript.sml | 63 (* matching function, that checks if a pair of variables match according *) 64 (* to a given pair of lists of variables; the lists are searched, and *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | lisp_printScript.sml | 647 if r4 && 4w = 0w then (* if true, first part of dot pair evaluated *) 661 else (* must be a pair *)
|
/seL4-l4v-10.1.1/HOL4/Manual/Logic/ |
H A D | semantics.tex | 60 (standard) signature $\Sigma_\Omega$, a sequent is a pair $(\Gamma, 1088 variables not occurring in $\sigma$. Such a pair would give rise
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
H A D | sexp.sml | 151 (* Add a pair (hol_name, acl2_name) to acl2_names after checking that *) 1714 (* An encap represents ENCAPSULATE and is a pair comprising the list of *)
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | sexp.sml | 151 (* Add a pair (hol_name, acl2_name) to acl2_names after checking that *) 1640 (* An encap represents ENCAPSULATE and is a pair comprising the list of *)
|