/seL4-l4v-master/isabelle/src/Doc/Logics_ZF/document/ |
H A D | FOL.tex | 3 \index{first-order logic|(} 6 nk}. Intuitionistic first-order logic is defined first, as theory 15 first-order terms is called \cldx{term} and is a subclass of \isa{logic}. 249 for first-order logic because they discard universally quantified 299 depth-first search, to solve subgoal~$i$. 302 best-first search (guided by the size of the proof state) to solve subgoal~$i$. 466 Q)\disj (Q\imp P)$. The first step is apply the 538 above. Its key step is its first rule, \tdx{exCI}, a classical 612 Classical first [all...] |
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics_ZF/document/ |
H A D | FOL.tex | 3 \index{first-order logic|(} 6 nk}. Intuitionistic first-order logic is defined first, as theory 15 first-order terms is called \cldx{term} and is a subclass of \isa{logic}. 249 for first-order logic because they discard universally quantified 299 depth-first search, to solve subgoal~$i$. 302 best-first search (guided by the size of the proof state) to solve subgoal~$i$. 466 Q)\disj (Q\imp P)$. The first step is apply the 538 above. Its key step is its first rule, \tdx{exCI}, a classical 612 Classical first [all...] |
/seL4-l4v-master/HOL4/src/parse/ |
H A D | qbuf.sml | 16 field #3 : the first fragment number of the remainder frag list 21 i) the first element of fld4 is a QUOTE element iff
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | congLib.sig | 46 * When simplifing a term t that matches x, where x contains x1, ... xn, * it first simplifies (x1 to y1 according to R1) then 93 * SIMP_CONV, it takes as the first argument the relation it
|
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/ |
H A D | emit_eval.sml | 398 val first = ref true value 406 out [if !first then 407 (first := false; "Registers:\t") 419 out [if !first then (first := false; "Registers:\t") else "\t\t", 428 val first = ref true value 433 out [if !first then (first := false; "Memory:") else "",
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Thm.sml | 12 (* An abstract type of first order logic theorems. *) 163 (* The literal L must occur in the first theorem, and the literal ~L must *)
|
/seL4-l4v-master/isabelle/src/Doc/Logics/document/ |
H A D | syntax.tex | 25 first-order logic, where $\exists$ has lower priority than $\disj$, 53 example, the formulae of first-order logic have type~$o$. Every
|
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | cond_cleanLib.sml | 11 in first (can (match_term pat) o concl) insts end 121 val th = first (can (find_term (fn tm => tm = ``Inst 0xF0013DECw``)) o concl) thms
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Thm.sml | 12 (* An abstract type of first order logic theorems. *) 163 (* The literal L must occur in the first theorem, and the literal ~L must *)
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/ |
H A D | syntax.tex | 25 first-order logic, where $\exists$ has lower priority than $\disj$, 53 example, the formulae of first-order logic have type~$o$. Every
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | PmatchHeuristics.sig | 25 choices. If the list is too short, the first column is 26 chosen. One should run this heuristic first with an empty list
|
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | SmtLib.sml | 173 "word_extract: second index larger than first" 177 "second index larger than first" 183 WARNING "translate_term" "word_extract: first index too large" 187 "first index too large" 358 (* SMT-LIB is first-order. Thus, functions can only be applied to 448 raise ERR "translate_term" "not first-order") (* handled below *) 460 raise ERR "translate_term" "not first-order") (* handled below *) 524 arguments to the term. (Because SMT-LIB is first-order,
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | EXPORT_PARSETREE.sml | 341 (* The first position is the expression, the second the type *) 432 (* The first position is the expression, the second the matches *) 449 (* The first position is the expression, the second the matches *) 459 | Andalso {location, first, second, ...} => 460 (location, exportList(getExportTree, SOME asParent) [first, second] @ commonProps) 462 | Orelse{location, first, second, ...} => 463 (location, exportList(getExportTree, SOME asParent) [first, second] @ commonProps) 482 (* The first position is the label, the second the type *)
|
/seL4-l4v-master/isabelle/src/Pure/Thy/ |
H A D | thy_syntax.scala | 172 first: Command, last: Command): Linear_Set[Command] = 174 val cmds0 = commands.iterator(first, last).toList 235 val first = next_invisible(cmds.reverse, first_unparsed) 238 reparse_spans(resources, syntax, get_blob, can_import, name, cmds, first, last))
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Thy/ |
H A D | thy_syntax.scala | 172 first: Command, last: Command): Linear_Set[Command] = 174 val cmds0 = commands.iterator(first, last).toList 235 val first = next_invisible(cmds.reverse, first_unparsed) 238 reparse_spans(resources, syntax, get_blob, can_import, name, cmds, first, last))
|
/seL4-l4v-master/HOL4/src/real/ |
H A D | selftest.sml | 62 fun pr1 t (Exn.Exn e) = "On first call, unexpected exn: " ^ 67 else "On first call, unexpected thm:\n " ^
|
/seL4-l4v-master/HOL4/examples/dev/dff/ |
H A D | nextScript.sml | 37 (* Definition of Next. Time t2 is the first (i.e. next) time after t1 *)
|
/seL4-l4v-master/HOL4/examples/ |
H A D | fol.sml | 2 * Some first order logic examples, using John Harrison's implementation *
|
/seL4-l4v-master/HOL4/polyml/modules/IntInfAsInt/ |
H A D | Integer.sml | 23 (* Define this first. It's explicitly referenced in the INTEGER signature. *)
|
/seL4-l4v-master/HOL4/src/HolQbf/ |
H A D | QbfLibrary.sml | 95 (* respect to the absolute value of its elements first component, [~]i. *) 180 (* coming first. *) 220 (* merge: merges two lists of tuples whose first components are integers *) 279 (* since variables are always bound innermost first, we simply
|
/seL4-l4v-master/HOL4/src/compute/examples/ |
H A D | Arith.sml | 38 (* Tricky case. The \y is first reduced weakly. Then \z must be reduced
|
/seL4-l4v-master/HOL4/src/num/arith/src/ |
H A D | Instance.sml | 31 re-instantiating. The first argument is a function for obtaining a
|
/seL4-l4v-master/HOL4/src/search/ |
H A D | dirGraphScript.sml | 2 (* Depth first traversal of directed graphs that can contain cycles. *)
|
/seL4-l4v-master/HOL4/tools/ |
H A D | win-config.sml | 7 | _ => (warn "Must specify HOLDIR as first and only argument\n";
|
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | arm_parserLib.sig | 88 (assumes the first add is narrow) */
|