/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Windows.sml | 559 (* The timeout and retry count apply only in the case of
|
/seL4-l4v-master/HOL4/examples/fermat/twosq/ |
H A D | iterateComputeScript.sml | 279 (* Idea: recursion with cutoff c, starting count j. *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_STATIC_LINK_AND_CASES.sml | 710 newNorefs := newAddr; (* increment count *)
|
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootScript.sml | 6656 (\state. loc <> 0 /\ (FDOM (SND state) = (IMAGE (\m. loc + m) (count n)))))))``, 6701 Q.ABBREV_TAC `s2 = (IMAGE (\m. m + x') (count n))` THEN 9545 if (~((IMAGE (\n'. loc + n') (count m)) SUBSET FDOM (SND s)) \/ (loc = 0)) then NONE else 9546 (SOME {(FST s, DRESTRICT (SND s) (COMPL (IMAGE (\n'. loc + n') (count m))))}))`; 9577 Q.ABBREV_TAC `loc_set = IMAGE (\n'. n' + ev) (count n)` THEN 9670 Q.ABBREV_TAC `locS = (IMAGE (\n'. ev + n') (count nv))` THEN 9848 `count 1 = {0}` by (
|
/seL4-l4v-master/HOL4/examples/simple_complexity/loop/ |
H A D | loopListScript.sml | 463 SUM (GENLIST f n) is better, corresponding to: SIGMA f (count n) 464 SUM_GENLIST_THM |- !f n. SUM (GENLIST f n) = SIGMA f (count n)
|
H A D | loopDecreaseScript.sml | 348 (* Define a hop function, count of hops to zero. *)
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | sptreeScript.sml | 589 ``domain (fromList l) = count (LENGTH l)``, 592 domain t UNION IMAGE ((+) i) (count (LENGTH l))`
|
/seL4-l4v-master/HOL4/examples/algebra/lib/ |
H A D | helperNumScript.sml | 3347 Hence s SUBSET count (SUC z) by SUBSET_DEF 3375 `s SUBSET (count (SUC z))` by metis_tac[IN_COUNT, SUBSET_DEF, LESS_EQ_TRANS] >>
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | CODEGEN_PARSETREE.sml | 344 (* Make an array to count the number of references to a pattern. 353 (* Increment the count for this pattern. *)
|
/seL4-l4v-master/HOL4/src/pred_set/src/more_theories/ |
H A D | wellorderScript.sml | 372 ``elsOf (fromNatWO n) = IMAGE INL (count n)``,
|
/seL4-l4v-master/HOL4/examples/AKS/machine/ |
H A D | countMacroScript.sml | 31 (* pre-load and open here for other count scripts. *)
|
/seL4-l4v-master/HOL4/examples/simple_complexity/lib/ |
H A D | bitsizeScript.sml | 413 (* Both 0 and 1 needs no halving to count. *)
|
/seL4-l4v-master/HOL4/examples/algebra/polynomial/ |
H A D | polyModuloRingScript.sml | 1001 = CARD count n by ZN_def
|
/seL4-l4v-master/HOL4/src/list/src/ |
H A D | rich_listScript.sml | 2884 `!n. LIST_TO_SET (COUNT_LIST n) = count n`, 3393 \\ `A SUBSET count (LENGTH ls)` by simp[Abbr`A`, SUBSET_DEF] 3394 \\ `B SUBSET count (SUC (LENGTH ls))` by simp[Abbr`B`, SUBSET_DEF]
|
H A D | listScript.sml | 3799 ���!f ls. IMAGE (\n. f (EL n ls)) (count (LENGTH ls)) = IMAGE f (set ls)���, 3870 ���!f n. LIST_TO_SET (GENLIST f n) = IMAGE f (count n)���,
|
/seL4-l4v-master/HOL4/examples/miller/prob/ |
H A D | prob_algebraScript.sml | 1554 >> Know `BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE f (count N))`
|
/seL4-l4v-master/seL4/manual/parts/ |
H A D | threads.tex | 539 instructions before resuming single-stepping. This skip-count can also be set in
|
/seL4-l4v-master/HOL4/examples/algebra/group/ |
H A D | groupCyclicScript.sml | 1113 the sum of phi(d) over all divisors d will count all elements in the group,
|
/seL4-l4v-master/HOL4/examples/algebra/finitefield/ |
H A D | ffAdvancedScript.sml | 935 = CARD (count (char r)) by GF_property
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | misc.tex | 809 incremented. A total count as well as counts per primitive inference 848 the argument \ml{x} and performs a count of inferences during this
|
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/ |
H A D | hol_defaxiomsScript.sml | 2183 > Matt says: The measure for (expt r i) is (abs (ifix i)). Intuitively, we count 2184 > down for positive exponents and count up for negative exponents
|
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | hol_defaxiomsScript.sml | 2153 > Matt says: The measure for (expt r i) is (abs (ifix i)). Intuitively, we count 2154 > down for positive exponents and count up for negative exponents
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | hol_defaxiomsScript.sml | 2149 > Matt says: The measure for (expt r i) is (abs (ifix i)). Intuitively, we count 2150 > down for positive exponents and count up for negative exponents
|
/seL4-l4v-master/HOL4/Manual/Description/ |
H A D | misc.tex | 889 incremented. A total count as well as counts per primitive inference 928 the argument \ml{x} and performs a count of inferences during this
|
/seL4-l4v-master/HOL4/examples/logic/ltl/ |
H A D | ltl2waaScript.sml | 2047 `{ f l | n <= l } ��� count (f n + 1)` by (
|