/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibSubst.sml | 102 fun check (a, b, (c, d)) = function 104 val (removed, dict') = M.foldl check (false, dict) dict
|
H A D | mlibUnits.sml | 52 fun check t = (unify_literals |<>| (dest_unit t) lit, t) function 54 case first (total check) (N.unify uns lit) of NONE => NONE
|
H A D | mlibModel.sig | 45 val check : model -> formula -> bool value
|
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibSimple.sig | 75 function to apply, a check when to apply and a theorem about how 76 to rewrite in case the check succeeds. For FST the entries would
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/ |
H A D | modelCheckLib.sig | 5 used to translate several model checking problems to a check for the 7 is used to check these properties. At the moment SMV and temporalLib by
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/lib/ |
H A D | libffi.exp | 332 proc check-flags { args } { 376 if [check-flags $args] {
|
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | file.scala | 155 def check(file: JFile) { if (pred(file)) result += file } 157 if (start.isFile) check(start) 163 if (include_dirs) check(path.toFile) 168 check(path.toFile)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/ |
H A D | build_docker.scala | 91 echo = true).check
|
/seL4-l4v-10.1.1/isabelle/src/Tools/VSCode/src/ |
H A D | vscode_spell_checker.scala | 51 if (spell_checker.check(word))
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_spell_checker.scala | 60 if (spell_checker.check(word))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | file.scala | 155 def check(file: JFile) { if (pred(file)) result += file } 157 if (start.isFile) check(start) 163 if (include_dirs) check(path.toFile) 168 check(path.toFile)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/ |
H A D | build_docker.scala | 91 echo = true).check
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/VSCode/src/ |
H A D | vscode_spell_checker.scala | 51 if (spell_checker.check(word))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_spell_checker.scala | 60 if (spell_checker.check(word))
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_encoderLib.sml | 89 fun check (f,m) b = (b () orelse raise ERR f (term_to_string m); I); function 91 fun check_is_15 s tm = check (s,tm) (fn _ => is_PC tm); 157 check ("encode_mode3", tm) (fn _ => width_okay 8 imm12) 160 check ("encode_mode3", tm) (fn _ => is_0 imm2) 233 check ("encode_branch", tm) (fn _ => is_T toarm orelse is_PC cond) 252 check ("encode_data_processing", tm) (fn _ => check_dp (opc,d,n)) 383 check ("encode_load_store", tm) (fn _ => is_0 imm8) 387 check ("encode_load_store", tm) (fn _ => is_0 imm8) 422 check ("encode_miscellaneous", pairSyntax.mk_pair (cond,tm)) 478 let val checkbr = check ("thumb_encode_branc [all...] |
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/src/ |
H A D | regexSemanticsScript.sml | 38 (* sanity check and helper lemmata *)
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Sanity.sig | 30 2 : no check
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_Script.sml | 33 if EVERY (\x. ~(x = NONE)) (XREAD_INSTR_BYTES n e s) (* check that the memory is there *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_Script.sml | 33 if EVERY (\x. ~(x = NONE)) (ZREAD_INSTR_BYTES n e s) (* check that the memory is there *)
|
/seL4-l4v-10.1.1/HOL4/polyml/modules/IntInfAsInt/ |
H A D | Makefile.in | 345 check-am: all-am 346 check: check-am 447 .PHONY: all all-am all-local check check-am clean clean-generic \
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | internal_functions.sml | 210 fun check s = function 217 case List.filter check files of 248 fun check p = function 262 smash (get_first check paths) 264 | NONE => if isUnix then "" else smash (check ".")
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | loop_bounds.py | 1 import check,search,problem,syntax,solver,logic,rep_graph,re namespace 4 from check import restr_others,split_visit_one_visit 196 checks = (check.single_loop_induct_step_checks (p, restrs, hyps, tag, 198 + check.single_loop_induct_base_checks (p, restrs, hyps, tag, 201 groups = check.proof_check_groups (checks) 203 (res, _) = check.test_hyp_group (rep, group) 518 hyp = check.mk_loop_counter_eq_hyp (p, split, restrs, n - 2) 563 checks = check.split_checks (p, (), hyps, split, tags = [asm_tag, c_tag]) 564 groups = check.proof_check_groups (checks) 567 (res, el) = check [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/include/ |
H A D | Makefile.in | 475 check-am: all-am 476 check: check-am 581 .PHONY: CTAGS GTAGS TAGS all all-am check check-am clean clean-generic \
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/man/ |
H A D | Makefile.in | 430 check-am: all-am 431 check: check-am 537 .PHONY: all all-am check check-am clean clean-generic clean-libtool \
|
/seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
H A D | QbfCertificate.sml | 163 (* check: proves or disproves the QBF 't' (see QDimacs.sml for the format of *) 178 fun check t dict (VALID (exts,lits)) = let function 352 Feedback.HOL_WARNING "QbfCertificate" "check" "final theorem has hyps" 356 Feedback.HOL_WARNING "QbfCertificate" "check" 362 | check t _ (INVALID (dict, cindex)) = 410 raise ERR "check" 414 raise ERR "check" 434 Feedback.HOL_WARNING "QbfCertificate" "check" "final theorem has hyps" 439 Feedback.HOL_WARNING "QbfCertificate" "check" "final theorem not F"
|