/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | gr_t.sml | 2 * gr_t.sml -- graph implementations based on balanced binary search tress 12 A graph is represented by pair (t,m) where t is a search tree
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | gr_t.sml | 2 * gr_t.sml -- graph implementations based on balanced binary search tress 12 A graph is represented by pair (t,m) where t is a search tree
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | gr_t.sml | 2 * gr_t.sml -- graph implementations based on balanced binary search tress 12 A graph is represented by pair (t,m) where t is a search tree
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/lisp/ |
H A D | a2ml.lisp | 237 (let ((pos (search *directory-separator-string* file :from-end t)))
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
H A D | separationLogicLib.sml | 202 fun search p = function 210 val thm2_opt = search p'; 219 search 400 (*search abstractions*) 435 (*search abstraction*) 450 (*search abstraction*)
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootLib.sml | 1187 (*destruct and search for points to*) 1211 (*destruct and search for points to*) 1308 (*destruct and search for points to*) 1329 (*destruct and search for points to*) 1417 (*destruct and search for points to*) 1465 (*destruct and search for points-to / array*) 1681 (*search lists*) 1786 (*search lists*) 1873 (*search lists*) 1945 (*search list [all...] |
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttSearch.sml | 42 (* Start and end of search *) 657 (* fake a node when a proof is found but no search is performed on this node *) 859 else (search_step (); debug_search "search step"; search_loop ()) 939 fun search thmpred tacpred glpred hammer goal = function 945 val _ = debug_search "End search loop"
|
H A D | tttLearn.sml | 3 (* DESCRIPTION : Learning from tactic calls during search and recording *)
|
H A D | tttMinimize.sml | 275 (* could be replaced by minimization search,
|
H A D | tttPredict.sml | 120 (* used during search *)
|
/seL4-l4v-10.1.1/HOL4/Manual/Interaction/ |
H A D | HOL-interaction.tex | 44 \item[~] Section \ref{search}:~~Searching for theorems and theories 288 \mysec{Searching for theorems and theories\label{search}} 317 Once theories has been opened (see Section~\ref{copy}), one can search for theorems in the current 340 The key-binding \texttt{M-h~m} (and the menu entry ``DB match'') will prompt for the term pattern to search for, and pass this query onto the HOL session (saving the need to type \texttt{print\_match~[]} and the enclosing quotation marks). 532 Section~\ref{search}) and the HTML reference (mentioned in
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/lambek/ |
H A D | ExampleScript.sml | 145 (* this time automatic proof search by arrow doesn't work: 148 Meson search level: ................Exception- Interrupt raised
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | term_grammar.sml | 797 fun search acc rs = function 803 PREFIX (BINDER blist) => search (search_blist acc blist) rest 805 search (search_rrlist (Prefix (valOf fixopt)) acc rrlist) 808 search (search_rrlist (Suffix (valOf fixopt)) acc rrlist) 811 search (search_rrlist (Infix(assoc, valOf fixopt)) acc rrlist) 813 | CLOSEFIX rrl => search (search_rrlist Closefix acc rrl) rest 814 | _ => search acc rest 817 search [] (rules G)
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | tactics.tex | 39 The idea of goal directed proof\index{goal directed proof search!reason for} is a simple one, well known in 40 artificial intelligence: to organize the search\index{proof construction!as tree search} as a tree, and to reverse 53 as a tree search, starting with a conjunctive goal 57 the difference is in the search, and in the preservation, if required, of 76 \index{goal directed proof search!concepts of|(} 82 a tree search strategy.} of 84 \index{justifications, in goal-directed proof search} 117 logical sense (of a sequence of theorems depending on inference\index{inferences, in HOL logic@inferences, in \HOL{} logic!in goal-directed proof search} rules) 213 basic logic, whether the proof is found by goal directed search [all...] |
H A D | conv.tex | 333 $c\ u$ fails are left unchanged.) The definition leaves open the search strategy; 335 \ml{DEPTH\_CONV}$\ c$\index{DEPTH_CONV@\ml{DEPTH\_CONV}!search strategy of} 370 in characterizing the search strategy of {\tt TOP\_DEPTH\_CONV} should 448 \noindent The search invoked by \ml{BETA\_RULE} 468 that used the second search strategy could be defined as shown below
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Solver.C | 411 | if conflict arose before search even started). 652 | search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&) -> [lbool] 664 lbool Solver::search(int nof_conflicts, int nof_learnts, const SearchParams& params) 729 // Return search-space coverage. Not extremely reliable. 823 status = search((int)nof_conflicts, (int)nof_learnts, params);
|
/seL4-l4v-10.1.1/HOL4/src/meson/src/ |
H A D | mesonLib.sml | 2 (* Version of the MESON procedure a la PTTP. Various search options. *) 505 (* Simple Prolog engine which organizes search and backtracking. *) 778 (* automated proof search!) *) 959 let val _ = if (!chatting = 1) then say "Meson search level: " else ()
|
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/ |
H A D | Intmap.sml | 29 * 1. The implementation is based on Binary search trees of Bounded
|
/seL4-l4v-10.1.1/HOL4/tools-poly/poly/ |
H A D | Binarymap.sml | 32 * 1. The implementation is based on Binary search trees of Bounded
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | trace_refute.py | 15 import search namespace 181 restrs = search.restr_others_both (p, restrs, 2, 2) 203 be the actual call node. a short breadth-first-search should hopefully
|
/seL4-l4v-10.1.1/HOL4/Manual/LaTeX/ |
H A D | ack.tex | 42 added material on first order proof search; and Tjark Weber, who wrote
|
/seL4-l4v-10.1.1/HOL4/examples/Crypto/TEA/ |
H A D | teaScript.sml | 221 (* and needs to be visible on the search path when using or loading teaML. *)
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Intro/document/ |
H A D | root.tex | 66 structures for expressing search procedures. Isabelle also provides
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Intro/document/ |
H A D | root.tex | 66 structures for expressing search procedures. Isabelle also provides
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | Socket.sml | 205 (* Do a linear search on the list - it's small. *) 215 (* Do a linear search on the list - it's small. *) 237 (* Do a linear search on the list - it's small. *) 247 (* Do a linear search on the list - it's small. *)
|