/seL4-l4v-10.1.1/graph-refine/ |
H A D | logic.py | 1049 # themselves. the search algorithm doesn't 1069 import search namespace 1074 return search.eval_model_expr ({}, eval_expr_solver[0], expr) 1194 import search namespace 1195 va = search.get_loop_var_analysis_at (p, loop_head)
|
H A D | solver.py | 2021 import search namespace 2025 b = search.eval_model (m, c) 2132 import search namespace 2134 return search.eval_model (m, sexpr)
|
/seL4-l4v-10.1.1/HOL4/Manual/Quick/ |
H A D | quick.tex | 195 \hol{Conv}{GSYM} \var{thm} & reverses the first equation(s) encountered in a top-down search \\ 269 \hol{DB}{find} \var{string} & search for theory element by name fragment \\
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | int-binary-map.sml | 33 * 1. The implementation is based on Binary search trees of Bounded
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | int-binary-map.sml | 33 * 1. The implementation is based on Binary search trees of Bounded
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | int-binary-map.sml | 33 * 1. The implementation is based on Binary search trees of Bounded
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | PmatchHeuristics.sml | 197 an exhaustive search heuristic-fun
|
H A D | dep_rewrite.sig | 43 (* or the term itself in the third case. The search is top-to-bottom,*)
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | metisTools.sml | 27 5: Log of each inference during proof search *)
|
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/ |
H A D | Intset.sml | 31 * 1. The implementation is based on Binary search trees of Bounded
|
/seL4-l4v-10.1.1/HOL4/tools/mllex/ |
H A D | mllex.sml | 362 let fun search [] = raise LOOKUP function 363 | search((k,item)::entries) = 366 else search entries 367 in search entrylist
|
/seL4-l4v-10.1.1/HOL4/developers/mlton-srcs/ |
H A D | Binarymap.sml | 101 * 1. The implementation is based on Binary search trees of Bounded
|
/seL4-l4v-10.1.1/isabelle/src/Doc/ |
H A D | preface.tex | 36 language and a fully automatic search would be impractical. Isabelle does
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/ |
H A D | preface.tex | 36 language and a fully automatic search would be impractical. Isabelle does
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | metis.sml | 86 description = "Skip the proof search for the input problems",
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | metis.sml | 86 description = "Skip the proof search for the input problems",
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
H A D | fp.tex | 289 {\S}\ref{sec:advanced-datatypes}; it closes with another case study, search 416 Tries are a classic search tree data structure~\cite{Knuth3-75} for fast 420 examined sequentially. Each letter determines which subtrie to search next.
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | fp.tex | 289 {\S}\ref{sec:advanced-datatypes}; it closes with another case study, search 416 Tries are a classic search tree data structure~\cite{Knuth3-75} for fast 420 examined sequentially. Each letter determines which subtrie to search next.
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | PairRules.sml | 241 let fun search m pthl = function 246 val (ff,fc) = search f pthl 247 and (bf,bc) = search b pthl 265 let val (bf,bc) = search b pthl' 276 snd (search mask assl)
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | lzPairRules.sml | 201 let fun search m pthl = function 206 val (ff,fc) = search f pthl 207 and (bf,bc) = search b pthl 225 let val (bf,bc) = search b pthl' 236 snd (search mask assl)
|
/seL4-l4v-10.1.1/HOL4/src/pred_set/Manual/ |
H A D | description.tex | 1340 internal \HOL\ search paths. A pathname to the library is added to the search 1342 \ml{pred\_sets}; and the \HOL\ help search path is updated with a pathname to 1345 After the search paths are updated, the actions taken by the load sequence for 1418 library updates the search path. 1428 this case, loading the library can (and will) update the search paths. But the 1439 theory (now accessible via the search path) becomes an ancestor of the current
|
/seL4-l4v-10.1.1/l4v/tools/haskell-translator/ |
H A D | lhs_pars.py | 1494 if dollar_lambda_regex.search(line): 1579 m = type_assertion.search(line) 2214 m = re.search(line) 2421 while record_getter.search(pat): 2801 m = modulename.search(line)
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Sledgehammer/document/ |
H A D | root.tex | 119 The result of a successful proof search is some source text that usually (but 424 proof is too difficult for it. Metis's search is complete for first-order logic 471 search is fully typed, and it also includes more powerful rules such as the 484 uses no type information at all during the proof search, which is more efficient 926 up to three slices are tried, with different weighted search strategies and 937 proof search.
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Sledgehammer/document/ |
H A D | root.tex | 119 The result of a successful proof search is some source text that usually (but 424 proof is too difficult for it. Metis's search is complete for first-order logic 471 search is fully typed, and it also includes more powerful rules such as the 484 uses no type information at all during the proof search, which is more efficient 926 up to three slices are tried, with different weighted search strategies and 937 proof search.
|
/seL4-l4v-10.1.1/HOL4/tools-poly/poly/ |
H A D | Binaryset.sml | 29 * 1. The implementation is based on Binary search trees of Bounded
|