/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Proof.h | 39 virtual void deleted(ClauseId c) {} function in struct:ProofTraverser 68 void deleted (ClauseId gone);
|
H A D | Proof.C | 162 void Proof::deleted(ClauseId gone) function in class:Proof 165 trav->deleted(abs(gone)); 403 trav.deleted(chain_id[0]-1); //HA: -1 to compensate for id_counter base 1
|
H A D | Main.C | 79 reportf("conflict literals : %-12"I64_fmt" (%4.2f %% deleted)\n", stats.tot_literals, (stats.max_literals - stats.tot_literals)*100 / (double)stats.max_literals); 164 void deleted(ClauseId c) { function in struct:Checker
|
H A D | Solver.C | 160 if (proof != NULL) proof->deleted(c->id());
|
/seL4-l4v-10.1.1/isabelle/Admin/Release/ |
H A D | isasync | 87 conservative in the sense that files are never deleted, thus garbage
|
/seL4-l4v-10.1.1/l4v/isabelle/Admin/Release/ |
H A D | isasync | 87 conservative in the sense that files are never deleted, thus garbage
|
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/mlyacclib/ |
H A D | MLY_parser2.sml | 426 toks' is the actual tokens (with positions and values) deleted, 438 of SOME(deleted,_,r',lp'') => 439 SOME(tok::deleted,l,r',lp'') 448 of SOME(deleted,l,r,lp) => 450 leftPos=l,rightPos=r,orig=deleted,
|
/seL4-l4v-10.1.1/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | parser2.sml | 408 toks' is the actual tokens (with positions and values) deleted, 420 of SOME(deleted,l',r',lp'') => 421 SOME(tok::deleted,l,r',lp'') 430 of SOME(deleted,l,r,lp) => 432 leftPos=l,rightPos=r,orig=deleted,
|
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | parser2.sml | 408 toks' is the actual tokens (with positions and values) deleted, 420 of SOME(deleted,l',r',lp'') => 421 SOME(tok::deleted,l,r',lp'') 430 of SOME(deleted,l,r,lp) => 432 leftPos=l,rightPos=r,orig=deleted,
|
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | CCSLib.sml | 200 summand to be then deleted by applying the idempotence law for summation. *)
|
H A D | StrongLawsConv.sml | 58 (* Find repeated occurrences of a summand to be then deleted by applying
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | api.tex | 218 invocation cannot be performed until either these objects are deleted or
|
H A D | cspace.tex | 240 Capabilities in seL4 can be deleted and revoked. Both methods 286 deleted as a result of the revoke. In this case the thread performing 289 capability that is the target of the revoke is deleted as a result of
|
H A D | threads.tex | 57 deleted. 415 if the I/O port capability is deleted for any reason the access will be correspondingly removed
|
H A D | objects.tex | 375 region have been deleted, the kernel will reset the watermark and start
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | zc2hs.cpp | 166 void deleted(ClauseId c) { function in struct:Checker
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Thm_cont.sml | 338 (* This version deleted for HOL version 1.12 [TFM 91.01.17] *)
|
H A D | Tactic.sml | 836 * Old version: deleted for HOL version 1.12 [TFM 91.01.17] *
|
/seL4-l4v-10.1.1/HOL4/Manual/Description/ |
H A D | version2.tex | 13 \LCF\ have been deleted and many `internal' \ML\ bindings have been 122 list the \ML\ bindings that have ben added and deleted in Version 2.0. 1243 \noindent have been deleted, and replaced by the constant specification: 1350 The \ML\ identifiers that have been added and deleted in Version 2.0 1430 deleted by mistake---please let us know if you want anything back.
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | version2.tex | 13 \LCF\ have been deleted and many `internal' \ML\ bindings have been 122 list the \ML\ bindings that have ben added and deleted in Version 2.0. 1243 \noindent have been deleted, and replaced by the constant specification: 1350 The \ML\ identifiers that have been added and deleted in Version 2.0 1430 deleted by mistake---please let us know if you want anything back.
|
H A D | HolSat.tex | 170 Normally, {\tt{HolSatLib}} will delete the files generated by the SAT solver, such as the output proof, counter-model, and result status. However, if \texttt{infile} is set, the files are not deleted, in case they are required elsewhere.
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/ |
H A D | CTT.tex | 590 Can assumptions be deleted after use? Not every occurrence of a type 594 can be deleted safely. In Type Theory, $+$-elimination with the assumption
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/ |
H A D | CTT.tex | 590 Can assumptions be deleted after use? Not every occurrence of a type 594 can be deleted safely. In Type Theory, $+$-elimination with the assumption
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Parse.sml | 918 but with "non-trivial" overloads deleted *)
|
/seL4-l4v-10.1.1/HOL4/src/rational/ |
H A D | fracScript.sml | 795 * deleted
|