/seL4-l4v-10.1.1/HOL4/src/pred_set/src/ |
H A D | pred_setScript.sml | 3216 val count_def = new_definition ("count_def", ``count (n:num) = {m | m < n}``); 3220 ``!m n. m IN count n = m < n``, 3226 ``count 0 = {}``, 3233 ``!n. count (SUC n) = n INSERT count n``, 3239 ``!n. FINITE (count n)``, 3247 ``!n. CARD (count n) = n``, 3257 ``(count n1 = count n2) <=> (n1 = n2)``, 3696 val NOT_IN_COUNT = Q.prove (`~ (m IN count [all...] |
H A D | pred_setSyntax.sml | 63 val (count_tm, mk_count, dest_count, is_count) = s1 "count"
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | Menu.sml | 535 val count = List.length mlist 560 let val count = List.length mlist value 562 val menu = alloc count (Cstruct [Cshort,Cshort,Cpointer Cchar])
|
H A D | Base.sml | 852 return a count of the number actually assigned. *) 877 val count = List.length l value 881 val vec = malloc(Word.fromInt count * sizea) 885 (vec, count)
|
/seL4-l4v-10.1.1/HOL4/src/holyhammer/legacy/ |
H A D | hh_tac.ml | 329 ((fun ty -> let count = !gcounter in 330 (gcounter := count + 1; 331 mk_var("_"^(string_of_int count),ty))),
|
/seL4-l4v-10.1.1/HOL4/examples/miller/prob/ |
H A D | prob_uniformScript.sml | 618 0 < n /\ a SUBSET count n ==> 650 >> Suff `e IN count (SUC n')` >- RW_TAC bool_ss [SPECIFICATION, IN_COUNT] 656 0 < n /\ a SUBSET count n /\ 2 * log2 (n + 1) <= t ==>
|
H A D | probScript.sml | 1635 (Q.SPECL [`f`, `n`, `count n`] 1745 BIJ c (count n) (range (FST o f)) ==> 1753 BIGUNION (IMAGE (\m. $= (c m) o FST o f) (count n))` 1754 >- (Suff `BIGUNION (IMAGE (\m. $= (c m) o FST o f) (count n)) = UNIV` 1788 (count n))) = 1792 (count n))) + 1897 (?c n. BIJ c (count n) (range (FST o f)))``, 2565 (IMAGE (\n. {s | ~c (FST (FUNPOW (UNCURRY b) n (a,s)))}) (count m))` 2966 (count m)))` 3067 (count [all...] |
/seL4-l4v-10.1.1/HOL4/tools/mllex/ |
H A D | mllex.sml | 511 | "count" => COUNT 930 val count = ref 0 value 1018 (count := !count+1; 1068 msg ("\nNumber of distinct rows = " ^ (Int.toString (!count))); 1070 (Int.toString (!count*(!CharSetSize)*(if !CharFormat then 1 else 8))));
|
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/ |
H A D | generalHelpersScript.sml | 118 `FINITE {f' n | n ��� count b }` suffices_by fs[IN_ABS,count_def] 1511 >> `U ��� (count N)` by ( 1552 `{a | ?k. a = (f i + k) MOD N } = count N` by ( 1559 >> `n ��� count N` by simp[count_def] 1568 >> `U = count N` 1572 by (`f i ��� count N` suffices_by metis_tac[] >> fs[count_def])
|
H A D | buechiAScript.sml | 62 ��� (a, r (j+1)) ��� aut.trans (r j) ��� at x j ��� a} DIFF (count k)` by ( 66 >> `FINITE (count k)` by metis_tac[FINITE_COUNT]
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | ConseqConv.sig | 221 not count 375 not count
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/kernel/ |
H A D | boot.c | 227 for (i = 0; i < mem_p_regs.count; i++) {
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
H A D | Useful.sig | 122 (* Lists: note we count elements from 0 *)
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibSupport.sml | 136 if small_space (M.size m) n (length (FV fm)) 1 then M.count m fm
|
H A D | mlibUseful.sig | 58 (* Lists: note we count elements from 0 *)
|
H A D | mlibModel.sml | 422 fun count m fm = function 432 chat ("count: " ^ formula_to_string fm ^ ": " ^
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | HM_Core_Cline.sml | 138 (wn "Ignoring non-positive job count"; t)
|
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/ |
H A D | SyntacticSugarScript.sml | 149 `count = NUM of num (* number *)
|
/seL4-l4v-10.1.1/HOL4/examples/diningcryptos/ |
H A D | extra_realScript.sml | 1168 (!n. 0 <= f n) /\ INJ j1 (count n1) UNIV /\ 1169 IMAGE j1 (count n1) SUBSET IMAGE j2 (count n2) ==> 1262 Q.SPECL [`h`, `s`, `count N INTER s`] o 1265 >> Know `FINITE (count N INTER s)` 1336 Q.SPECL [`h`, `s`, `count n INTER s`] o 1339 >> Know `FINITE (count n INTER s)`
|
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | ind_types.sml | 302 val count = ref 0 value 305 temp_binding (safepfx ^ current_theory() ^ Int.toString (!count)) 307 if (not (null (decls nm))) then (count := !count + 100; 309 else (count := !count + 1; nm)
|
/seL4-l4v-10.1.1/HOL4/src/real/ |
H A D | seqScript.sml | 1767 ?k. IMAGE f (count N) SUBSET count k CROSS count k``, 1786 ?N. count k CROSS count k SUBSET IMAGE f (count N)``, 1789 Q.SPECL [`f`, `UNIV CROSS UNIV`, `count k CROSS count k`] o
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_seq_monadScript.sml | 807 let count = FST (coprocessors.load_count inst coprocessors.state) 810 (forT 0 (count - 1) readm)
|
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_seq_monadScript.sml | 813 let count = FST (coprocessors.load_count inst coprocessors.state) 816 (forT 0 (count - 1) readm)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | gc_share_phase.cpp | 128 void sortList(PolyObject *head, POLYUNSIGNED nItems, POLYUNSIGNED &count); 375 // Clear the entries in the hash table but not the sharing count. 468 // Clear the entries in the hash table but not the sharing count.
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/ |
H A D | X86FOREIGNCALL.sml | 184 | _ => raise InternalError "rtsCall: Abi/argument count not implemented" 283 | _ => raise InternalError "rtsCall: Abi/argument count not implemented"
|