/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttMinimize.sig | 6 datatype Proof = type 8 | Then of (Proof * Proof) 9 | Thenl of (Proof * Proof list) 13 val minimize_proof : Proof -> Proof 14 val reconstruct : goal -> Proof -> string
|
H A D | tttSearch.sig | 23 ProofError | ProofSaturated | ProofTimeOut | Proof of string
|
H A D | tacticToe.sml | 203 | Proof s => 331 NONE => debug_eproof ("Proof status: Time Out") 342 debug_eproof ("Proof found: " ^ newstac) 354 | ProofSaturated => debug_proof "Proof status: Saturated" 355 | ProofTimeOut => debug_proof "Proof status: Time Out" 356 | Proof s => debug_proof ("Proof found: " ^ s)
|
H A D | tttMinimize.sml | 154 datatype Proof = type 156 | Then of (Proof * Proof) 157 | Thenl of (Proof * Proof list)
|
/seL4-l4v-10.1.1/l4v/misc/pysymbols/isasymbols/ |
H A D | __init__.py | 16 from .proof import Proof namespace
|
H A D | proof.py | 19 p = Proof('True \\<and> True') 30 class Proof(object): class in inherits:object
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | Makefile | 6 ln -fs ../minisat/Proof.o 9 ln -fs ../minisat/Proof.h 13 g++ -O3 Proof.o File.o zc2hs.cpp -o zc2hs
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
H A D | ellipticTools.sig | 17 (* Proof tools. *)
|
H A D | ellipticTools.sml | 23 (* Proof tools. *)
|
H A D | fieldTools.sig | 35 (* Proof tools. *)
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Proof.h | 0 /*****************************************************************************************[Proof.h] 32 // A "listner" for the proof. Proof events will be passed onto (online mode) or replayed to 45 class Proof { class 58 Proof(); // Offline mode -- proof stored to a file, which can be saved, compressed, and/or traversed. 59 Proof(ClauseId goal); // Offline mode -- for pre-initialising c2fp 60 Proof(ProofTraverser& t); // Online mode -- proof will not be stored. 79 void compress (Proof& dst, ClauseId goal = ClauseId_NULL); // 'dst' should be a newly constructed, empty proof.
|
H A D | Proof.C | 0 /*****************************************************************************************[Proof.C] 20 #include "Proof.h" 63 // Proof logging: 65 Proof::Proof() function in class:Proof 75 Proof::Proof(ProofTraverser& t) function in class:Proof 83 ClauseId Proof::addRoot(vec<Lit>& cl, ClauseId orig_root_id) 109 void Proof::beginChain(ClauseId start) 118 void Proof [all...] |
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | holmakebuild.sml | 13 ("*** Proof of \n " ^ Parse.term_to_string t ^ "\n*** failed (used CHEAT).\n")
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/cantor/ |
H A D | Cantor.ml | 1 % Proof of Cantor's Theorem %
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Prog_Prove/document/ |
H A D | root.tex | 37 \chapter{Logic and Proof Beyond Equality}
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Prog_Prove/document/ |
H A D | root.tex | 37 \chapter{Logic and Proof Beyond Equality}
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Proof.sml | 6 structure Proof :> Proof = structure 139 handle Error err => raise Bug ("Proof.pp: shouldn't fail:\n" ^ err); 195 raise Bug ("Proof.recontructSubst: shouldn't fail:\n" ^ err); 215 raise Bug ("Proof.recontructResolvant: shouldn't fail:\n" ^ err); 221 val () = Print.trace LiteralSet.pp "Proof.reconstructEquality: cl" cl 272 "Proof.reconstructEquality: candidates" candidates 281 raise Bug ("Proof.recontructEquality: shouldn't fail:\n" ^ err); 309 val () = Print.trace Thm.pp "Proof.thmToInference: th" th 318 val () = Print.trace ppThmInf "Proof [all...] |
H A D | Proof.sig | 6 signature Proof = signature
|
H A D | Tptp.sml | 901 {inference : Proof.inference, 927 Proof.Axiom cl => LiteralSet.functions cl 928 | Proof.Assume atm => Atom.functions atm 929 | Proof.Subst (sub,_) => Subst.functions sub 930 | Proof.Resolve (atm,_,_) => Atom.functions atm 931 | Proof.Refl tm => Term.functions tm 932 | Proof.Equality (lit,_,tm) => 954 Proof.Axiom cl => LiteralSet.relations cl 955 | Proof.Assume atm => NameAritySet.singleton (Atom.relation atm) 956 | Proof [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Proof.sml | 6 structure Proof :> Proof = structure 139 handle Error err => raise Bug ("Proof.pp: shouldn't fail:\n" ^ err); 195 raise Bug ("Proof.recontructSubst: shouldn't fail:\n" ^ err); 215 raise Bug ("Proof.recontructResolvant: shouldn't fail:\n" ^ err); 221 val () = Print.trace LiteralSet.pp "Proof.reconstructEquality: cl" cl 272 "Proof.reconstructEquality: candidates" candidates 281 raise Bug ("Proof.recontructEquality: shouldn't fail:\n" ^ err); 309 val () = Print.trace Thm.pp "Proof.thmToInference: th" th 318 val () = Print.trace ppThmInf "Proof [all...] |
H A D | Proof.sig | 6 signature Proof = signature
|
H A D | Tptp.sml | 901 {inference : Proof.inference, 927 Proof.Axiom cl => LiteralSet.functions cl 928 | Proof.Assume atm => Atom.functions atm 929 | Proof.Subst (sub,_) => Subst.functions sub 930 | Proof.Resolve (atm,_,_) => Atom.functions atm 931 | Proof.Refl tm => Term.functions tm 932 | Proof.Equality (lit,_,tm) => 954 Proof.Axiom cl => LiteralSet.relations cl 955 | Proof.Assume atm => NameAritySet.singleton (Atom.relation atm) 956 | Proof [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/dff/ |
H A D | dffScript.sml | 3 (* DESCRIPTION : Proof that a unit delay is implemented by a simple *) 59 (* Proof that there is no simple SINGLE abstraction from *)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/Hahn_Banach/document/ |
H A D | root.tex | 69 \part {Lemmas for the Proof} 76 \part {The Main Proof}
|
/seL4-l4v-10.1.1/isabelle/src/HOL/Hahn_Banach/document/ |
H A D | root.tex | 69 \part {Lemmas for the Proof} 76 \part {The Main Proof}
|