/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | enumeralScript.sml | 651 (* "OU" for "Ordered Union" - used for intermediate (tree, binary list) pair
|
H A D | fmapalScript.sml | 109 the argument-value pair; "v" is for "value [only]". *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | MATCH_COMPILER.sml | 521 let (* The argument is a pair consisting of the
|
H A D | CODEGEN_PARSETREE.sml | 1497 functions as a mutually recursive pair. Try putting
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | tactics.tex | 151 pair selectors and constructor. 172 type \ml{subgoals}, \ie\ a pair whose first component is a list of 1247 pair \ml{($gll$,$pl$)} of a subgoal list and a proof function, where
|
H A D | libraries.tex | 52 \ml{Parse}. Le teorie fornite includono \theoryimp{pair}, 2655 The pair of provided theorems must state 2663 the first component of the pair. Assuming the \simpset{} fragment
|
H A D | theories.tex | 743 � definito nella teoria \theoryimp{pair}. I valori di tipo 806 L'operatore di tipo {\small\verb%prod%} � definito invocando \ml{new\_type\_definition}\index{new_type_definition@\ml{new\_type\_definition}} con questo teorema che risulta nell'asserazione nella teoria \ml{pair} dell'assioma definizionale \index{assiomi!non-primitivi, della logica HOL@non-primitivi, della logica \HOL{}!per prodotti} \index{assiomi!nella teoria bool@nella teoria \ml{bool}} \ml{prod\_TY\_DEF} mostrato di sotto. 1033 \index{termini, nella logica HOL@termini, nella logica \HOL{}!pair|)}
|
/seL4-l4v-master/HOL4/examples/AKS/machine/ |
H A D | countPolyScript.sml | 2263 (* Polynomial weak addition (by pair-wise add in mod n) *) 2277 h <- (head p) + (head q) MOD n // pair-wise add of heads 3013 return list_add p1 p2 // add the results, pair-wise
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/model/ |
H A D | arm8Script.sml | 3918 Var("acctype",CTy"AccType"),bVar"excl",bVar"pair",bVar"rn_unknown", 3921 ITE(bVar"pair", 3980 Var("acctype",CTy"AccType"),bVar"excl",bVar"pair",Var("Rs",FTy 5), 3986 Bop(And,bVar"pair",EQ(Var("Rt",FTy 5),Var("Rt2",FTy 5)))), 4002 Bop(And,bVar"pair",EQ(Var("Rs",FTy 5),Var("Rt2",FTy 5)))), 4053 bVar"pair",bVar"rn_unknown",bVar"rt_unknown",
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | functionEncodeLib.sml | 3567 val pair = #predicate scheme value 3570 val R = list_mk_abs([y,x],mk_conj(mk_comb(pair,x), 4130 val recs = foldl (fn ((b,c),a) => map (pair b o mk_encoder)
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | parse_term.sml | 222 val msg = "Grammar ambiguous on token pair "^
|
H A D | term_pp.sml | 35 val dest_pair = sdest_binop (",", "pair") (PP_ERR "dest_pair" "");
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Tptp.sml | 24 {name = ",", arity = 2, tptp = "pair"},
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Tptp.sml | 24 {name = ",", arity = 2, tptp = "pair"},
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
H A D | stateLib.sml | 333 | {Thy = "pair", Args = [a, b], Tyop = "prod"} =>
|
/seL4-l4v-master/HOL4/examples/algebra/group/ |
H A D | finiteGroupScript.sml | 637 (* Split element of (s1 o s2) into a left-right pair *)
|
/seL4-l4v-master/isabelle/src/Doc/Logics/document/ |
H A D | HOL.tex | 199 exists a unique pair $(x,y)$ satisfying~$P\,x\,y$. 1042 $\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/ |
H A D | HOL.tex | 199 exists a unique pair $(x,y)$ satisfying~$P\,x\,y$. 1042 $\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General
|
/seL4-l4v-master/HOL4/examples/algebra/polynomial/ |
H A D | polyGCDScript.sml | 353 Step 1: get a coprime pair 2473 Step 1: get a coprime pair
|
H A D | polyWeakScript.sml | 418 e.g. for pair-addition, it is easy to show: p || q = q || p, p || q || t = p || (q || t). 459 How about multiplication, which involves cpair, pair and shift?
|
/seL4-l4v-master/HOL4/src/list/src/ |
H A D | listScript.sml | 22 are "arithmetic", "pair", "pred_set" and those theories behind the 272 (* for mapping a curried binary function down a pair of lists: *)
|
/seL4-l4v-master/HOL4/src/pattern_matches/ |
H A D | patternMatchesLib.sml | 594 build for all rows the pair of the pattern + the patterns 1898 The patterns are represented as a pair of
|
/seL4-l4v-master/HOL4/src/quotient/examples/ |
H A D | ind_rel.sml | 384 Two theorems are returned as a pair, (thm1, thm2). The first is a
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Sledgehammer/document/ |
H A D | root.tex | 710 \item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers
|
/seL4-l4v-master/isabelle/src/Doc/Sledgehammer/document/ |
H A D | root.tex | 710 \item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers
|