/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | SmtLib_Parser.sml | 27 overloading, there may be several dictionary entries for the same 51 the same dictionary. 6. To deal with numerals and other tokens
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibClause.sml | 508 ever see the same hit list for another new clause C generated by an 521 But this gives the same new clause as the hit list
|
/seL4-l4v-master/isabelle/src/Doc/Intro/document/ |
H A D | foundations.tex | 235 $P(x)$ into a function, this is the same as saying that $\lambda x.P(x)$ 245 in the same way. Other binding operators are also easily handled; for 282 b$. The two equality symbols have the same logical meaning. 285 The syntax of the meta-logic is formalized in the same manner 392 typical of quantifier rules always have the same form, namely `$x$ not free in 438 they must not, for example, assign different types to the same constant. 471 coexist at the same time, and you may work in each of these during a single 735 x$. At the same time, lifting introduces a dependence upon~$x$. It replaces
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | basics.tex | 161 Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type. 195 and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/ |
H A D | foundations.tex | 235 $P(x)$ into a function, this is the same as saying that $\lambda x.P(x)$ 245 in the same way. Other binding operators are also easily handled; for 282 b$. The two equality symbols have the same logical meaning. 285 The syntax of the meta-logic is formalized in the same manner 392 typical of quantifier rules always have the same form, namely `$x$ not free in 438 they must not, for example, assign different types to the same constant. 471 coexist at the same time, and you may work in each of these during a single 735 x$. At the same time, lifting introduces a dependence upon~$x$. It replaces
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | basics.tex | 161 Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type. 195 and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type
|
/seL4-l4v-master/HOL4/examples/algebra/linear/ |
H A D | FiniteVSpaceScript.sml | 83 val _ = set_fixity "||" (Infixl 500); (* same as + in arithmeticScript.sml *) 347 (c) Define linear combination = VSUM (MAP f (ZIP (slist, vlist))) of same length
|
/seL4-l4v-master/HOL4/examples/algebra/monoid/ |
H A D | monoidScript.sml | 138 (* Monoid and Group share the same type *) 157 to achieve the same effect.
|
H A D | submonoidScript.sml | 124 val _ = set_fixity "<<" (Infix(NONASSOC, 450)); (* same as relation *) 336 val _ = set_fixity "mINTER" (Infix(NONASSOC, 450)); (* same as relation *)
|
/seL4-l4v-master/HOL4/src/coretypes/ |
H A D | DefnBase.sml | 492 (* now make var-columns use same vars as first row, except that 493 non-pattern variables in the first row can't be the same as variables
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | x86assembly_masm64.S | 221 ; This implements atomic subtraction in the same way as atomic_decrement
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | CODEGEN_PARSETREE.sml | 447 same time create a debugging environment if required. *) 486 (* The instance type is not necessarily the same as the type 702 we need to pass this along in the same way as when making bindings. *) 823 records in the same way but we have the problem of 954 (* This exception is treated in the same way as a local 1089 this declaration within the same "let..in..end" block. *) 1201 back at exactly the same offset we got them from. *) 1674 Set the local addresses at the same time. *)
|
H A D | BaseParseTreeSig.sml | 223 patterns in each clause. It checks that they are the same in each
|
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | SALGen.sml | 316 ( print("STOP: The source program (FIL) is invalid! (e.g. all variables are not of the same type)\n");
|
/seL4-l4v-master/HOL4/examples/fsub/ |
H A D | kernel_subtypingScript.sml | 254 same bound variable in the "other" position of the relation. By
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | PmatchHeuristics.sml | 43 (* assumption: rowL noteq [], and all rows have same length *)
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | totoTacs.sml | 41 and we need only preserve the same for all products of conversions. *)
|
/seL4-l4v-master/HOL4/src/num/ |
H A D | numLib.sml | 77 (* If the variables x and z are the same, the `z` instance will be primed. *)
|
/seL4-l4v-master/HOL4/src/rational/ |
H A D | schneiderUtils.sml | 117 (* These tactics do exactly the same as the tactics above, but *)
|
/seL4-l4v-master/HOL4/Manual/Description/ |
H A D | HolQbf.tex | 65 Finally, \ml{decide} does the same job as \ml{decide\_prenex} but accepts QBFs
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | HolQbf.tex | 65 Finally, \ml{decide} does the same job as \ml{decide\_prenex} but accepts QBFs
|
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/ |
H A D | sexpScript.sml | 430 (* (complex-rationalp #c(3 0)) ; nil, since #c(3 0) is the same as 3 *) 455 (* (complex x 0) ; same as x, for rational numbers x *) 465 (* The reader macro #C (which is the same as #c) provides a convenient way *) 467 (* #C(x y) is read to the same value as (complex x y). *)
|
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | sexpScript.sml | 430 (* (complex-rationalp #c(3 0)) ; nil, since #c(3 0) is the same as 3 *) 455 (* (complex x 0) ; same as x, for rational numbers x *) 465 (* The reader macro #C (which is the same as #c) provides a convenient way *) 467 (* #C(x y) is read to the same value as (complex x y). *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | COPIER.sml | 229 are the same as they were. *)
|
H A D | TYPETREESIG.sml | 123 (* The same as generalise but with a function that looks up types. *)
|