/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Rule.sig | 270 val factor' : Thm.clause -> Subst.subst list
|
H A D | Tptp.sml | 781 type clause = literal list; type 817 fun clauseFromThm th = clauseFromLiteralSet (Thm.clause th); 1848 | CnfGoal of (formulaName * clause) list 1923 fun addCnf role ((name,clause),(norm,cnf)) = 1924 if List.exists (equalBooleanLiteral true) clause then (norm,cnf) 1927 val cl = List.mapPartial (total destLiteral) clause 1930 val src = CnfClauseSource (name,clause) 2395 val cls = List.map Thm.clause (Proof.parents inference) 2445 val cl = Thm.clause th
|
H A D | Rewrite.sml | 169 literalsReducible order known id (Thm.clause th); 335 val (neq,_) = mkNeqConvs order (Thm.clause th) 397 rewriteIdLiteralsRule' order known redexes id (Thm.clause th) th;
|
H A D | problems.sml | 216 (lit ==> clause) ==> (lit \/ clause <=> clause)`},
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Rule.sig | 270 val factor' : Thm.clause -> Subst.subst list
|
H A D | Tptp.sml | 781 type clause = literal list; type 817 fun clauseFromThm th = clauseFromLiteralSet (Thm.clause th); 1848 | CnfGoal of (formulaName * clause) list 1923 fun addCnf role ((name,clause),(norm,cnf)) = 1924 if List.exists (equalBooleanLiteral true) clause then (norm,cnf) 1927 val cl = List.mapPartial (total destLiteral) clause 1930 val src = CnfClauseSource (name,clause) 2395 val cls = List.map Thm.clause (Proof.parents inference) 2445 val cl = Thm.clause th
|
H A D | Rewrite.sml | 169 literalsReducible order known id (Thm.clause th); 335 val (neq,_) = mkNeqConvs order (Thm.clause th) 397 rewriteIdLiteralsRule' order known redexes id (Thm.clause th) th;
|
H A D | problems.sml | 216 (lit ==> clause) ==> (lit \/ clause <=> clause)`},
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | BASE_PARSE_TREE.sml | 220 patterns in each clause. It checks that they are the same in each 221 clause. *)
|
H A D | BaseParseTreeSig.sml | 223 patterns in each clause. It checks that they are the same in each 224 clause. *)
|
H A D | TYPECHECK_PARSETREE.sml | 1643 may be more than one clause in a function binding but each 1652 (* Just look at the first clause for the moment. *) 1698 fun processClause (clause as FValClause {dec, exp, line, ...}) = 1723 (* This clause as a parsetree object for error messages. *) 1724 mkFunDeclaration([mkClausal([clause], line)], explicit, implicit, line) 1731 name ^ " has already been bound in this clause."); 1806 assigns the result type for each clause in the fun but 1809 (* The type of this clause is a function type. *) 1816 typeMismatch("Type of clause does not match the type of previous clauses.",
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Induction.sml | 377 (if is_imp(concl thm') (* recursive calls in this clause *) 458 (* A clause of the case_thm can have one of the following forms: *) 464 (* the clause. The reason for this is that "proved_cases" needs to align *) 471 fun match_clause pat clause = 473 val (V,tm) = strip_exists clause 479 of ([],[]) => clause
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
H A D | lisp_extractLib.sml | 808 (* derive assum clause *) 822 val clause = case ind of value 824 val clause = prove(forall_goal, value 829 in clause end 833 val clause = prove(i |> concl |> rand, value 842 in clause end 845 val _ = add_assum_clause clause
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | folMapping.sml | 429 val prettify_thm = (mlibThm.AXIOM o map prettify_formula o mlibThm.clause); 724 val hol_lits = map (fol_literal_to_hol parm) (clause fol_th) 737 val (sub, hol_lits') = f [] [] (zip (clause fol_th) hol_lits) 753 val (a, b) = partition (equal fl o fst) (zip (clause fth) hls) 785 val n = mlibUseful.index (equal fol_lit) (clause fol_th)
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | Z3_ProofReplay.sml | 88 The input clause (including "t") is really treated as a set of 91 its disjuncts may even be spread throughout the input clause). 93 in the input clause. 145 val clause = Thm.concl (List.hd thms) value 146 val clause_imp_t = prove_from_disj dict clause 148 Thm.MP (Thm.DISCH clause clause_imp_t) (List.hd thms)
|
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
H A D | ho_proverTools.sml | 65 datatype clause = CLAUSE of vars * literal list; type 67 datatype fact = FACT of clause * thm susp; 72 type clause_rule = clause -> (substitution * clause * rule) list; 79 (* Literal and clause operations. *) 256 (* Replace clause variables in a fact with fresh ones. *)
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | polytypicLib.sml | 705 of SOME (var_list,clause) => raise (dexn ("The variables; " ^ xlist_to_string term_to_string var_list ^ 706 " are free in the clause: " ^ term_to_string clause)) 881 (* a) there can be no free variables in any clause except fni *) 889 (* a) there can be no free variables in any clause except fni *) 1016 fun conv clause = 1019 (op:: (strip_comb (rand (lhs (snd (strip_forall clause)))))) 1023 clause 1189 fun is_double_term_target (scheme:translation_scheme) funcs clause term = 1199 (is_single_constructor scheme clause orels [all...] |
H A D | acl2encodeLib.sig | 120 (* a) Convert to clause form, using *)
|
H A D | functionEncodeLib.sml | 1544 (* Returns a list of clause * thm where if: *) 1546 (* clause(i) = ``f (Ci x y z) a b c *) 1571 (* Converts a function defined using clause structure to use case *) 1588 (* The algorithm terminates if this clause does not have a free variable *) 1593 (* reflection of this clause and adds it to the list of missing calls. *) 2993 (* Converts a missing clause to a limit *) 3012 ("Missing clause: " ^ term_to_string missing ^ 3020 (* Calculates the nested theorems required for a missing clause limit: *) 3179 (* Limit theorems: |- destructed clause ==> full clause *) [all...] |
/seL4-l4v-10.1.1/HOL4/src/meson/src/ |
H A D | mesonLib.sml | 429 (* Insert new goal's negation in ancestor clause, given refinement. *) 609 (* Creation of tagged contrapositives from a HOL clause. *) 927 (* time if there is a proof based on the first support clause with similar *) 928 (* size. It would be easy to separate out the support-clause trying (and *)
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Prim_rec.sml | 90 message = ("Failed to match LHSes in clause "^Int.toString cnum)} 437 fun clause (a,c) = mk_eq(list_mk_comb(v,c::arg_list), function 440 list_mk_conj (ListPair.map clause (arg_list, clist)) 1285 fun mk_clause clause = 1286 let val (lhs,rhs) = (dest_eq o #2 o strip_forall) clause 1791 fun clause n = let 1800 val clauses = sepby " | " (List.tabulate(n, clause))
|
H A D | Pmatch.sml | 61 * clause in a function definition. 751 val clause_s = if new_rows = 1 then " clause " else " clauses "
|
/seL4-l4v-10.1.1/HOL4/src/pfl/ |
H A D | index.sml | 435 let fun fn_of clause = fst(strip_comb(lhs(snd(strip_forall clause))))
|
/seL4-l4v-10.1.1/isabelle/src/Doc/ |
H A D | preface.tex | 32 An inference rule in Isabelle is a generalized Horn clause. Rules are
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/ |
H A D | preface.tex | 32 An inference rule in Isabelle is a generalized Horn clause. Rules are
|