| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | HM_Core_Cline.sml | 187 { help = "don't check which Holmake was last used", long = ["nolmbc"],
|
| /seL4-l4v-10.1.1/HOL4/tools/unicode-grep/ |
| H A D | ugrep.sml | 253 {help = "No line-length check", long = ["nolinelen"], short = "",
|
| /seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
| H A D | skiTools.sml | 93 else if occurs tm1 tm2 then raise ERR "ski_unify" "occurs check"
|
| /seL4-l4v-10.1.1/HOL4/examples/unification/triangular/first-order/ |
| H A D | walkScript.sml | 197 (* vwalk with rhs check *)
|
| /seL4-l4v-10.1.1/HOL4/developers/discussion/ |
| H A D | overloading-extension.tex | 105 avoid this problem because we can just check each monomorphic
|
| /seL4-l4v-10.1.1/HOL4/examples/Crypto/AES/ |
| H A D | aesScript.sml | 194 (* Sanity check *)
|
| /seL4-l4v-10.1.1/HOL4/examples/Crypto/MARS/ |
| H A D | MARSScript.sml | 292 (* Sanity check *)
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | lazyTools.sml | 109 (* quick check that lazification works *)
|
| /seL4-l4v-10.1.1/isabelle/src/HOL/Bali/document/ |
| H A D | root.tex | 75 \item A ``definite assignment'' check
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/HOL/Bali/document/ |
| H A D | root.tex | 75 \item A ``definite assignment'' check
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Subst.sml | 234 else if Term.freeIn v tm then raise Error "Subst.unify: occurs check"
|
| /seL4-l4v-10.1.1/isabelle/src/HOL/MicroJava/document/ |
| H A D | introduction.tex | 40 \item A ``definite assignment'' check
|
| /seL4-l4v-10.1.1/HOL4/polyml/basis/ |
| H A D | Word8.sml | 110 (* Use Word.scan but check that the result is in the range. *)
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Subst.sml | 234 else if Term.freeIn v tm then raise Error "Subst.unify: occurs check"
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/HOL/MicroJava/document/ |
| H A D | introduction.tex | 40 \item A ``definite assignment'' check
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/ |
| H A D | Datatype.sml | 370 fun check i = function
376 else (check i ; via (i + 1))
419 fun check j = function
423 check (j + 1))
425 if check 0 then (List.app zero_column b; (b, rest))
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Nitpick/document/ |
| H A D | root.tex | 109 satisfiable, while the locale is being developed. To check this, it suffices to
176 To check whether Kodkodi is successfully installed, you can try out the example
822 Let's check a property involving $\textit{even}'$. To make up for the
1032 bisimilarity check is then performed \textsl{after} the counterexample has been
1033 found to ensure correctness. If this after-the-fact check fails, the
1038 predicate or as an after-the-fact check) to prevent spurious counterexamples:
1062 In the first \textbf{nitpick} invocation, the after-the-fact check discovered
1067 problem and performing the after-the-fact check is to specify a low
1260 If the monotonicity check fails but we believe that the formula is monotonic (or
1437 as $b$'s) and check the
[all...] |
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Nitpick/document/ |
| H A D | root.tex | 109 satisfiable, while the locale is being developed. To check this, it suffices to
176 To check whether Kodkodi is successfully installed, you can try out the example
822 Let's check a property involving $\textit{even}'$. To make up for the
1032 bisimilarity check is then performed \textsl{after} the counterexample has been
1033 found to ensure correctness. If this after-the-fact check fails, the
1038 predicate or as an after-the-fact check) to prevent spurious counterexamples:
1062 In the first \textbf{nitpick} invocation, the after-the-fact check discovered
1067 problem and performing the after-the-fact check is to specify a low
1260 If the monotonicity check fails but we believe that the formula is monotonic (or
1437 as $b$'s) and check the
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | term_grammar.sml | 769 fun check rrec a = function
781 | rr :: rest => recurse (check rr acc) rest
1011 fun check c = function
1016 fupdate_numinfo (update_assoc (check c, stropt)) G
1081 val realc = check c
1092 fupdate_numinfo (List.filter (fn (k,v) => k <> (check c))) G
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/ |
| H A D | compile.sig | 435 (* (?x. A) /\ B --> ?x. A /\ B (check x not free in B) *)
436 (* A /\ (?x. B) --> ?x. A /\ B (check x not free in A) *)
|
| /seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
| H A D | SmtLib_Parser.sml | 497 | "check-sat" =>
499 val _ = dest_state "check-sat"
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | IntDP_Munge.sml | 496 fun check(t, free_p) = function
512 not (isSome (HOLset.find (not o check) dodgy_subterms))
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibModel.sml | 402 chat ("check: valuation=" ^ valuation_to_string v ^ ".\n")
407 fun check m fm = check1 (FV fm) m fm; function
|
| /seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
| H A D | elf_correlate.py | 15 from graph_refine.check import *
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
| H A D | CODETREE_LAMBDA_LIFT.sml | 131 (* Lambdas - check the function body and any recursive uses. *)
360 (* If it's a local we have to check that it's not one of our
|