/seL4-l4v-10.1.1/HOL4/polyml/ |
H A D | Makefile.in | 206 RECURSIVE_TARGETS = all-recursive check-recursive cscopelist-recursive \ 956 && $(MAKE) $(AM_MAKEFLAGS) check \ 993 echo " (check DESTDIR support)"; \ 1006 check-am: all-am 1007 $(MAKE) $(AM_MAKEFLAGS) check-local 1008 check: check-recursive 1122 .MAKE: $(am__recursive_targets) all check-am install-am install-strip 1125 am--refresh check check [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Waiting.sml | 117 fun check ((parm,model),z) = function 121 val {T,F} = Model.check Model.interpretClause n model fv cl 126 List.foldl check 1.0 (zip parms models)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolymain/ |
H A D | Makefile.in | 545 check-am: all-am 546 check: check-am 655 .PHONY: CTAGS GTAGS TAGS all all-am check check-am clean clean-generic \
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibMeson.sml | 329 fun check a' = a' = g' function 331 List.exists (check o formula_subst env) 342 fun check a' = a' = g' function 344 List.exists (check o formula_subst env) 406 (* Only check the meter every CHECK_PERIOD inferences to save time *) 430 fun check (s' as {depth = n', ...} : state) = function 433 f (c o check) s
|
H A D | mlibMatch.sml | 69 else if occurs x tm then raise Error "unify: occurs check"
|
H A D | mlibResolution.sml | 151 | SOME (dcl,sos) => check set sos n dcl 152 and check set sos n (d,cl) = function
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | debug.py | 18 import check namespace 690 checks = check.proof_checks (p, proof) 701 checks = check.proof_checks (p, proof) 702 groups = check.proof_check_groups (checks) 706 (res, el) = check.test_hyp_group (rep, group) 721 assert bits[:4] == ['Time', 'taken', 'to', 'check'] 770 p = check.build_problem (pair) 844 hyps = check.init_point_hyps (p)
|
H A D | inst_logic.py | 15 import check namespace
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Preterm.sml | 614 fun check(Comb{Rator, Rand, Locn}) = function 615 check Rator >> check Rand >> 653 | check (Abs{Bvar, Body, Locn}) = (check Bvar >> check Body) 654 | check (Constrained{Ptm,Ty,Locn}) = 655 check Ptm >> ptype_of Ptm >- (fn ptyp => 681 | check _ = ok 683 check [all...] |
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | zc2hs.cpp | 457 bool check = false; // verify the proof if true local 469 check = true; 503 // (check) and save proof 506 if (check) { // quick check
|
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
H A D | patternMatchesLib.sig | 219 (* check whether they can be *) 266 To check, whether the match is exhaustive, check whether 274 the flag is set to true, an exhaustiveness check is 397 Such a nchotomy theorem is often handy. We use it to check for 457 the precondition is ~F, but the user has to check. *)
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Traverse.sml | 223 fun check r = case !r of NONE => () function 260 (check lim_r; 263 (check lim_r ;
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/lambek/ |
H A D | ExampleScript.sml | 46 (* check if a given sentence has category s *) 52 (* Example 1: check simple sentences in (arrow NL) *) 88 (* Example 2: check complex sentences in Natural Deduction *) 129 (* Example 3: check complex sentences in Natural Deduction *)
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | match_goal.sig | 47 1. Parse quotation in context of goal (and check no free vars ending with _)
|
/seL4-l4v-10.1.1/HOL4/src/IndDef/ |
H A D | selftest.sml | 85 (* check MONO_COND *)
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | bitstringLib.sml | 52 fun check P err thm = function 131 check numLib.is_numeral (ERR "v2n_CONV" "not ground") 209 (* Equality check for any ground term combinations of ``v2w [..]`` and 231 then check is_bool (ERR "word_eq_CONV" "not ground")
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | TheoryPP.sml | 406 fun check tys = function 409 val axl = check "Axm" axioms 410 val defl = check "Def" definitions 411 val thml = check "Thm" theorems
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
H A D | DEBUGGERSIG.sml | 60 (* Create a local break point and check the global and local break points. *)
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Graphview/ |
H A D | mutator_dialog.scala | 327 private class Text_Field_Input(txt: String, check: String => Boolean = (_: String) => true) 336 foreground = if (check(text)) default_foreground else graphview.error_color
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | ListPair.sml | 100 (* Is it better to check the lengths first? *)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Graphview/ |
H A D | mutator_dialog.scala | 327 private class Text_Field_Input(txt: String, check: String => Boolean = (_: String) => true) 336 foreground = if (check(text)) default_foreground else graphview.error_color
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Solver.h | 209 inline void check(bool expr) { assert(expr); } function
|
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibParameters.sml | 77 (*check whether something should be done*) 333 (*check whether something should be done*)
|
/seL4-l4v-10.1.1/HOL4/examples/misc/ |
H A D | wardScript.sml | 215 fun check (p1, (_, (res1, _)), s1) (p2, (_, (res2, _)), s2) = function 217 fun checkl t = List.mapPartial (fn t' => if check t t' then SOME (t,t')
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | ElementSet.sml | 310 fun adds acc set = foldl check acc set 312 and check (elt,acc) = function
|