Searched refs:search (Results 26 - 50 of 150) sorted by relevance

123456

/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmetisTools.sig15 5: Log of each inference during proof search *)
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/
H A DquantHeuristicsLibSimple.sml4 (* to unwind than to the full search of quantifier *)
39 term -> (* var to search a guess for *)
40 term -> (* term to search in *)
88 (* search functions *)
H A DquantHeuristicsLibBase.sig135 are a record of theorems, conversion and full heuristics used during proof search. *)
253 If the search is aborted, because the depth is not big enough, a warning
254 is printed. Decrease for speed and increase if the warning appears and you want to search deeper.
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttSetup.sml4 (* search *)
H A DtttRecord.sml428 clean_subdirl "bool" ttt_search_dir ["debug","search","proof"];
434 (* Proof search *)
435 clean_subdirl thy ttt_search_dir ["debug","search","proof"];
H A DtacticToe.sml189 debug_t "search" (search thmpred tacpred glpred hammer) goal
/seL4-l4v-10.1.1/HOL4/src/res_quan/src/
H A DCond_rewrite.sml149 (* fn is a search function which returns a list of matches in the format *)
156 (* This tactic uses the search function fn to find any matches of Q in *)
191 (* search_top_down carries out a top-down left-to-right search for *)
/seL4-l4v-10.1.1/HOL4/examples/ind_def/
H A DalgebraScript.sml157 (* completed by a simple search for the proof of the conclusion using *)
223 (* rule induction on MTRACE P A, followed by semi-automatic search for *)
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/
H A DSolver.h102 lbool search (int nof_conflicts, int nof_learnts, const SearchParams& params);
194 double progress_estimate; // Set by 'search()'.
/seL4-l4v-10.1.1/graph-refine/
H A Dinst_logic.py13 import search namespace
/seL4-l4v-10.1.1/HOL4/Manual/Description/
H A DQuantHeuristics.tex32 core, there is a modular, syntax driven search for instantiation.
33 This search consists of a collection of interleaved heuristics. Users
110 parameters essentially configure, which heuristics are used during the guess-search. If
219 A special (degenerated) use of the framework, is turning guess search off completely and
248 They just search for gap guesses without any free variables.
258 guess-search. There are predefined parameters that handle
342 A very powerful, yet simple technique for teaching the guess search
475 Dichotomies can be exploited for guess search.
H A Dversion2.tex136 \noindent The search path mechanism has been revised in various ways.
139 Library pathnames are now no longer on the default search path, nor
140 are they added to the search path when a library is loaded (it is
144 The initial search path is now:
163 The \ml{install} function now sets the search path to:
194 library load-files to update the \HOL\ search path and help search
198 search path as follows:
259 internal search path used by \HOL\ to find online help files. The help
260 search pat
[all...]
/seL4-l4v-10.1.1/HOL4/src/unwind/Manual/
H A Ddescription.tex36 help\index{help!updating search path} search path. The help search path is
38 library. After updating the help search path, the \ML\ functions in the
48 Updating help search path
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DTerm.sml190 fun search [] = NONE function
191 | search ((path,tm) :: rest) =
195 Var _ => search rest
200 search (subtms @ rest)
203 fn tm => search [([],tm)]
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DTerm.sml190 fun search [] = NONE function
191 | search ((path,tm) :: rest) =
195 Var _ => search rest
200 search (subtms @ rest)
203 fn tm => search [([],tm)]
/seL4-l4v-10.1.1/HOL4/src/string/Manual/
H A Ddescription.tex401 \ml{load\_library} is to update the internal \HOL\ search paths. A pathname to
402 the \ml{string} library is added to the search path, so that theorems may be
404 help search path is updated with a pathname to online help files for the \ML\
407 After updating search paths, the load sequence for \ml{string} depends on the
474 updates the search path.
484 In this case, loading the library can and will update the search paths, as
495 accessible via the search path) becomes an ancestor of the current theory, this
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/
H A DQuantHeuristics.tex32 core, there is a modular, syntax driven search for instantiation.
33 This search consists of a collection of interleaved heuristics. Users
110 parameters essentially configure, which heuristics are used during the guess-search. If
219 A special (degenerated) use of the framework, is turning guess search off completely and
248 guess-search. There are predefined parameters that handle
332 A very powerful, yet simple technique for teaching the guess search
465 Dichotomies can be exploited for guess search.
H A Dversion2.tex136 \noindent The search path mechanism has been revised in various ways.
139 Library pathnames are now no longer on the default search path, nor
140 are they added to the search path when a library is loaded (it is
144 The initial search path is now:
163 The \ml{install} function now sets the search path to:
194 library load-files to update the \HOL\ search path and help search
198 search path as follows:
259 internal search path used by \HOL\ to find online help files. The help
260 search pat
[all...]
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/
H A DLK.tex440 duplication, we employ best-first search:
572 rules require a search strategy, such as backtracking.
616 search.
650 and this can only be discovered by search. The tactics given below permit
677 applies {\tt repeat_goal_tac} using depth-first search to solve subgoal~$i$.
701 applies {\tt step_tac} using depth-first search to solve subgoal~$i$.
705 applies {\tt step_tac} using best-first search to solve subgoal~$i$. It is
/seL4-l4v-10.1.1/isabelle/src/Doc/Nitpick/document/
H A Droot.tex872 \S\ref{scope-of-search}.
1183 %option in \S\ref{scope-of-search} for details.
1737 (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
1746 (\S\ref{scope-of-search}) are implicitly enabled,
1845 \label{scope-of-search}
1854 {\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
1855 (\S\ref{scope-of-search}).}
1893 is specified by the \textit{bits} (\S\ref{scope-of-search}) option. By default,
1902 {\small See also \textit{bits} (\S\ref{scope-of-search}) an
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/
H A DLK.tex440 duplication, we employ best-first search:
572 rules require a search strategy, such as backtracking.
616 search.
650 and this can only be discovered by search. The tactics given below permit
677 applies {\tt repeat_goal_tac} using depth-first search to solve subgoal~$i$.
701 applies {\tt step_tac} using depth-first search to solve subgoal~$i$.
705 applies {\tt step_tac} using best-first search to solve subgoal~$i$. It is
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Nitpick/document/
H A Droot.tex872 \S\ref{scope-of-search}.
1183 %option in \S\ref{scope-of-search} for details.
1737 (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
1746 (\S\ref{scope-of-search}) are implicitly enabled,
1845 \label{scope-of-search}
1854 {\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
1855 (\S\ref{scope-of-search}).}
1893 is specified by the \textit{bits} (\S\ref{scope-of-search}) option. By default,
1902 {\small See also \textit{bits} (\S\ref{scope-of-search}) an
[all...]
/seL4-l4v-10.1.1/HOL4/src/res_quan/Manual/
H A Ddescription.tex246 search function \ml{search\_top\_down}. This function determines how to
248 search function, other conditional rewriting strategy can be
249 implemented. The details of the tactics and search functions can be
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/
H A Delf_correlate.py16 import graph_refine.search as search namespace
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/
H A DtranslationsLib.sig25 * tells the function whether to search for multiple occurences of

Completed in 273 milliseconds

123456