/seL4-l4v-master/HOL4/examples/miller/prob/ |
H A D | prob_trichotomyTools.sml | 24 fun chain f seq 0 = [] function 25 | chain f seq n = 30 th :: chain f seq (n - 1) 36 Count.apply (chain ``prob_trichotomy`` ``prob_pseudo 103 95 75 0``) 10;
|
/seL4-l4v-master/HOL4/src/tfl/examples/sorting/ |
H A D | sortingScript.sml | 20 * a "chain" predicate that holds just when the relation R holds between *
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Proof.h | 33 // (offline mode) this class. Each call to 'root()' or 'chain()' produces a new clause. The first 34 // clause has ID 0, the next 1 and so on. These are the IDs passed to 'chain()'s 'cs' parameter. 38 virtual void chain (const vec<ClauseId>& cs, const vec<Var>& xs) {} function in struct:ProofTraverser
|
H A D | Proof.C | 142 trav->chain(chain_id, chain_var); 273 case -2 : // a chain that has been visited before. write it out now 302 case -1 : // this root/chain has not been visited before 317 } else { // if chain, process antecedent clauses first 324 c2c[id] = -2; // means a chain that has been visited but not written out yet 405 trav.chain(chain_id, chain_var);
|
H A D | Main.C | 149 void chain (const vec<ClauseId>& cs, const vec<Var>& xs) { function in struct:Checker
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | matchTools.sml | 46 fun chain [] = [] function 47 | chain [_] = [] 48 | chain (x :: (xs as y :: _)) = (x, y) :: chain xs; 146 fun vunify_type tyvarP = vunifyl_type tyvarP [] o chain; 212 fun vunify varP = vunifyl varP ([], []) o chain;
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | TYPEIDCODESIG.sml | 52 val defaultTypeVarMap: (int->int) * level -> typeVarMap (* The end of the chain. *) 57 (* Mark in the cache chain that some type constructors are new. *)
|
H A D | TYPETREESIG.sml | 65 (* Follow a chain of unified type variables *)
|
/seL4-l4v-master/HOL4/src/HolSat/ |
H A D | minisatParse.sml | 80 (* parse resolution chain *) 94 (* parse and resolve a chain : assumes all dependencies already calculated *) 155 in if isch then readTrace lfn cl sva vc clauseth fin (id+1) (* chain*) 162 (*build the clause/chain list *)
|
/seL4-l4v-master/HOL4/src/num/reduce/src/ |
H A D | Arithconv.sml | 251 and chain = INST [xv |-> xn, yv |-> yn, pv |-> pn, value 254 MP (MP (MP chain p1) p2) p3 283 and chain = INST [xv |-> xn, yv |-> yn, pv |-> pn, value 286 MP (MP (MP chain p1) p2) p3
|
/seL4-l4v-master/seL4/manual/tools/ |
H A D | gen_invocations.py | 34 arch_types = list(itertools.chain(*syscall_stub_gen.init_arch_types(WORD_SIZE).values()))
|
/seL4-l4v-master/HOL4/src/coretypes/ |
H A D | posetScript.sml | 92 ``chain ((s,r) : 'a poset) c <=> 267 chain (s,r) c /\ lub (s,r) c x ==> 274 chain (s,r) c /\ glb (s,r) c x ==>
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | wotScript.sml | 70 `chain (C:'x set set) = !a b. a IN C /\ b IN C ==> a cpl b`; 89 `uncl (c:'x set set) = !w. w SUBSET c /\ chain w ==> BIGUNION w IN c`; 104 (* We will prove, in imitation of Halmos/Zermelo/Zorn, chain (t0) . *) 130 (* We set out to prove that t0 is a chain. *) 217 (* "Since the union of a chain of comparable sets is comparable... ." *) 242 val chain_t0 = prove (``chain (t0:'x set set)``, 254 (* Imitation of gAC_lem for t0, now known to be a chain: *)
|
/seL4-l4v-master/HOL4/src/pred_set/src/more_theories/ |
H A D | wellorderScript.sml | 1084 `!c. chain c R ==> upper_bounds c R <> {}` 1445 val chain = new_definition ("chain", value 1448 val _ = overload_on ("chain",``Chain``); 1464 ``!r:'a#'a->bool s:'a->bool. chain r s = chain s r``, 1465 REWRITE_TAC [chain, chain_def] THEN SET_TAC []); 1476 (!P. chain P r ==> upper_bounds P r <> {}) ==> 1479 (!P. chain(r) P ==> (?y. fl(r) y /\ !x. P x ==> r(x,y))) ==> 1485 (!t. chain [all...] |
/seL4-l4v-master/HOL4/examples/logic/folcompactness/ |
H A D | folPropScript.sml | 99 >- ((* upper bounds of chain t *) 100 rename [���chain t _���, ���upper_bounds t _ ��� ������] >>
|
/seL4-l4v-master/HOL4/examples/set-theory/vbg/ |
H A D | ordinalScript.sml | 16 chain A R C ��� C ��� A ��� ���x y. x ��� C ��� y ��� C ��� R x y ��� R y x
|
/seL4-l4v-master/isabelle/src/HOL/SPARK/Manual/document/ |
H A D | intro.tex | 117 \caption{\SPARK{} program verification tool chain} 121 tool chain for the verification of \SPARK{} programs. HOL-\SPARK{} processes declarations
|
/seL4-l4v-master/l4v/isabelle/src/HOL/SPARK/Manual/document/ |
H A D | intro.tex | 117 \caption{\SPARK{} program verification tool chain} 121 tool chain for the verification of \SPARK{} programs. HOL-\SPARK{} processes declarations
|
/seL4-l4v-master/HOL4/src/pred_set/src/ |
H A D | set_relationScript.sml | 1346 chain s r = 1368 { k | chain k r /\ k <> {} /\ 1369 !C. chain C r /\ C SUBSET k /\ 1377 `!x s r. chain s r /\ x IN s ==> x IN domain r /\ x IN range r`, 1399 `chain C r /\ C SUBSET k2 /\ C SUBSET k1` 1445 chain (BIGUNION (fchains r)) r /\ 1477 chain C r /\ 1611 (!t. chain t r ==> upper_bounds t r <> {})
|
/seL4-l4v-master/graph-refine/ |
H A D | stack_logic.py | 880 chain = [] 896 chain.append (fname) 897 tag = 'fun%d' % len (chain) 901 if chain == []: 903 recursion_trace.append (' created fun chain %s' % chain)
|
/seL4-l4v-master/HOL4/src/unwind/ |
H A D | unwindLib.sml | 493 fun loops_containing_line line graph chain = 495 (filter (fn (_,predecs) => tmem (Lib.trye hd chain) predecs) graph) 496 val not_in_chain = filter (fn line => not (tmem line chain)) successors 497 val new_chains = map (fn line => line::chain) not_in_chain 501 in if tmem line successors then (rev chain)::new_loops
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | zc2hs.cpp | 152 void chain (const vec<ClauseId>& cs, const vec<Var>& xs) { function in struct:Checker 308 // create minisat chain for a "CL" line of zChaff proof trace 327 // create minisat chain for a "VAR" line of zChaff proof trace 351 // create minisat chain for "CONF" line of zChaff proof trace
|
/seL4-l4v-master/HOL4/src/datatype/record/ |
H A D | RecordType.sml | 446 1. that a complete chain of updates over any value is 447 equivalent to a chain of updates over ARB. This particular
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | ForeignMemory.sml | 152 (* It would be possible to chain the free list in the C memory
|
/seL4-l4v-master/HOL4/examples/imperative/ |
H A D | necec2010.sml | 267 Given a list of assumptions, converts them into a chain of refinements.
|