Searched defs:proof (Results 1 - 25 of 35) sorted by relevance

12

/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DZ3_Proof.sml63 type proof = (int, proofterm) Redblackmap.dict type
H A DZ3.sml116 val proof = Z3_ProofParser.parse_stream (ty_dict, tm_dict) value
H A DZ3_ProofParser.sml333 val proof = extend_proof proof (proofterm_i value
393 val proof = parse_proof get_token value
[all...]
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/
H A Dtool.tex
/seL4-l4v-10.1.1/HOL4/Manual/Tutorial/
H A Dtool.tex
/seL4-l4v-10.1.1/isabelle/src/Doc/Intro/document/
H A Dgetting.tex[all...]
H A Dfoundations.tex[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Intro/document/
H A Dgetting.tex[all...]
H A Dfoundations.tex[all...]
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DProof.sig21 type proof = (Thm.thm * inference) list type
39 val proof : Thm.thm -> proof value
H A DProof.sml23 type proof = (Thm.thm * inference) list; type
401 fun proof th = function
H A Dmetis.sml220 val proof = value
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DProof.sig21 type proof = (Thm.thm * inference) list type
39 val proof : Thm.thm -> proof value
H A DProof.sml23 type proof = (Thm.thm * inference) list; type
401 fun proof th = function
H A Dmetis.sml220 val proof = value
/seL4-l4v-10.1.1/HOL4/src/proofman/
H A DManager.sig5 datatype proof type
[all...]
H A DproofManagerLib.sig4 type proof = Manager.proof type
[all...]
H A DManager.sml12 datatype proof = GOALSTACK of goalStack.gstk history type
H A DproofManagerLib.sml12 type proof = Manager.proof type
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/
H A DMain.C170 void checkProof(Proof* proof, ClauseId goal = ClauseId_NULL) argument
204 char* proof = NULL; local
[all...]
H A DSolver.h175 Proof* proof; // Set this directly after constructing 'Solver' to enable proof logging. Initialized to NULL. member in class:Solver
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibThm.sig28 val proof : thm -> (thm * inference') list value
H A DmlibThm.sml367 val proof = rev o thm_foldr (fn (th,l) => (th, inference th) :: l) []; value
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/poly/
H A Dholfoot_command_line.sml97 val proof = proofManagerLib.p () value
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/zc2hs/
H A Dzc2hs.cpp171 void checkProof(Proof* proof, ClauseId goal = ClauseId_NULL) argument
455 char* proof = NULL; // the name of the output minisat proof trac local
[all...]

Completed in 203 milliseconds

12