/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/ |
H A D | bibtex.scala | 45 /** check database **/ 674 cwd = tmp_dir.file).check
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/ |
H A D | bibtex.scala | 45 /** check database **/ 674 cwd = tmp_dir.file).check
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/ |
H A D | def_cnf.sml | 29 val spine_disj = HolKernel.spine_binop (total dest_disj) (*FIXME: fold is_lit check into this *)
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | PairedLambda.sml | 302 (*check which variables are used / unused. Abort if
|
H A D | PairRules.sml | 343 fun check V tm = function 346 if is_comb tm then check V (rand tm) orelse check V (rator tm) else 347 if is_abs tm then check (set_diff V (bvar tm)) (body tm) 350 check (FVL [p] empty_tmset) t
|
/seL4-l4v-10.1.1/HOL4/examples/Crypto/RC6/ |
H A D | RC6Script.sml | 309 (* Sanity check *)
|
/seL4-l4v-10.1.1/HOL4/help/src-sml/ |
H A D | ParseDoc.sml | 317 (* check that the second field is the "TYPE" one *)
|
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
H A D | Recftn.sml | 250 (* check if there's an "allelse" clause for this type; 278 (* if it was in here, check to make sure it wasn't in there 319 (* we have a new type to report info and check functions for *)
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | OmegaMLShadow.sml | 422 fun check ((f,d),a) = let function 431 (dbfold check NONE ptree; true) handle return_false => false 443 we just need to check that the maximum of the lower bounds is less
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibOmega.sml | 474 fun check ((f,d),a) = let function 483 (dbfold check NONE ptree; true) handle return_false => false 495 we just need to check that the maximum of the lower bounds is less
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | RW.sml | 104 * I could check that the lhs is not embedded in the rhs, but that wouldn't 271 * "sys_var" could be more rigorous in its check, but we don't 322 * a constant, but I don't currently check that.
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | basis2002.sml | 680 fun check i j = function 684 check (i - 1) (j - 1)) 686 check (size small - 1) (size big - 1)
|
H A D | Holmake_types.sml | 97 | #"$" => (* check for well-formed variable *) let
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Prim_rec.sml | 1333 fun check [] = true function 1334 | check ((x,y)::rst) = (x=y) andalso check rst 1336 check (zip opvars rhs_heads) 1386 (* The standard versions of these (in Conv) check that the term being
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | cearTools.sml | 152 (*val nabsv = Real.ceil(log2(Real.fromInt(k+1))) (* to check if new abstract state requires another abs var to be added *)*) 526 (* check whether abstract counterexample atr has concrete counterpart upto nth state of the abstract counterexample trace*) 633 (* check whether abstract counterexample atr has concrete counterpart *) 635 (* to check if full counterexample was discovered we can compare the length of the returned counterexample with atr *) 641 val ctr = check_ace' atr I1 T1 state Ric astate h atrsz (* check if there is a full concrete counterexample *)
|
H A D | lzPairRules.sml | 342 then let fun check V tm = function 345 if is_comb tm then check V (rand tm) orelse check V (rator tm) else 346 if is_abs tm then check (set_diff V [bvar tm]) (body tm) 348 in check (free_vars p) t
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | Makefile.in | 347 RECURSIVE_TARGETS = all-recursive check-recursive cscopelist-recursive \ 1646 && $(MAKE) $(AM_MAKEFLAGS) check \ 1683 echo " (check DESTDIR support)"; \ 1696 check-am: all-am 1697 check: check-recursive 1865 am--refresh check check-am clean clean-cscope clean-generic \
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | TYPECHECK_PARSETREE.sml | 354 to check the type here. *) 485 we don't check for constructor status. *) 695 check that the id is not a constructor. *) 998 identifier. This is needed to check "well-formedness" in signatures. *) 1237 (* Construct an environment to check for duplicate declarations. 1284 (* In the check environment *) 1582 (* Must check that the expression is of the form FN match. *)
|
/seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/ |
H A D | Opentheory.sml | 108 (* alternative: check if it's actually a literal with lit_conv, and
|
/seL4-l4v-10.1.1/HOL4/src/proofman/ |
H A D | goalStack.sml | 64 * system of ML is not strong enough to check that.
|
/seL4-l4v-10.1.1/HOL4/examples/logic/ |
H A D | PropLogicScript.sml | 407 (* Sanity check, not used later. *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_opsemScript.sml | 305 (* check whether rm requires a lock, i.e. specifies a memory access *)
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/ |
H A D | bdd.sig | 219 to check that r really represents a varSet therefore it should be
|
/seL4-l4v-10.1.1/HOL4/examples/unification/triangular/first-order/ |
H A D | walkstarScript.sml | 298 (* occurs check, which is (proved) equivalent to vars o walkstar *)
|
/seL4-l4v-10.1.1/HOL4/examples/Crypto/Serpent/Reference/ |
H A D | Serpent_Reference_TransformationScript.sml | 721 (* parity check is the same as counting EVEN or ODD.
|