| /seL4-l4v-10.1.1/HOL4/polyml/basis/ |
| H A D | Date.sml | 129 Note: We're assuming the Gregorian calendar. *)
|
| H A D | OS.sml | 412 If we're in the root directory we get the root directory.
413 If we're in a path that ends with a component
|
| /seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
| H A D | Z3_ProofReplay.sml | 59 later retrieval, to avoid re-reproving them *)
762 (* re-ordering conjunctions and disjunctions *)
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | CooperCore.sml | 273 (* we're rewriting something like c | (x +/- y * d) + e *)
461 whether or not we're under a negation; the following are
|
| H A D | integerScript.sml | 127 val (le, re) = pair_from_list
129 val eqv = MK_COMB(AP_TERM eqop le,re)
524 on the boolean negation, but we're doing so to put it back at the
|
| H A D | CooperShell.sml | 314 (* assume that there are no quantifiers below the one we're eliminating *)
|
| /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
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
| H A D | CommonDialog.sml | 660 (* Most of the fields are unchanged so we're better off extracting
1157 (* Since we're not going to set all of it we need to zero it. *)
|
| /seL4-l4v-10.1.1/HOL4/Manual/Description/ |
| H A D | misc.tex | 108 dependencies between files, (re)compile plain ML code, (re)compile and
109 execute theory scripts, and (re)compile the resulting theory modules.
139 and re-compiling and re-executing them.
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | misc.tex | 108 dependencies between files, (re)compile plain ML code, (re)compile and
109 execute theory scripts, and (re)compile the resulting theory modules.
139 and re-compiling and re-executing them.
|
| H A D | tactics.tex | 13 without having to be re-proved. The second,
1726 extended to such cases by re-conceiving the stack as an array\index{assumptions!as array}\index{array, of assumptions}, and by
1824 and re-assumes the others.)
2124 having to re-program them in \ML. This avoids the danger of
|
| /seL4-l4v-10.1.1/HOL4/src/coalgebras/ |
| H A D | lbtreeScript.sml | 574 either at the top of the tree in which case we're done, or it
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
| H A D | ConsThms.sml | 227 and we're done *)
|
| /seL4-l4v-10.1.1/HOL4/src/n-bit/ |
| H A D | blastLib.sml | 771 re-introduce subtraction
|
| /seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
| H A D | tttUnfold.sml | 4 (* Produces SML strings re-usable in different context. *)
|
| /seL4-l4v-10.1.1/HOL4/examples/lambda/other-models/ |
| H A D | pure_dBScript.sml | 864 show that dbeta matches up with beta on terms, and then we're all done *)
|
| /seL4-l4v-10.1.1/HOL4/examples/CCS/ |
| H A D | ExpansionScript.sml | 250 (* `P expands Q` if P R Q for some expansion R, re-defined by co-induction
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
| H A D | CODETREE_STATIC_LINK_AND_CASES.sml | 588 Because we're using "word" here any negative values are treated as
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
| H A D | DEBUGGER_.sml | 374 could depend on whether we're only counting line numbers or whether we
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
| H A D | rules.tex | 730 would see the danger and would re-orient the equality, but in more complicated
1832 We have derived a new fact; if re-oriented, it might be
1833 useful for simplification. After re-orienting it and putting $n=1$, we
1917 To re-orient the equation requires the symmetry rule:
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
| H A D | rules.tex | 730 would see the danger and would re-orient the equality, but in more complicated
1832 We have derived a new fact; if re-oriented, it might be
1833 useful for simplification. After re-orienting it and putting $n=1$, we
1917 To re-orient the equation requires the symmetry rule:
|
| /seL4-l4v-10.1.1/seL4/manual/parts/ |
| H A D | cspace.tex | 250 re-use.
|
| H A D | threads.tex | 283 attempt to re-configure \texttt{bp\_num} for Breakpoint or Watchpoint usage until
|
| /seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
| H A D | regexpScript.sml | 715 (* is not easy to determine, so we're conservative here and just say that *)
|
| /seL4-l4v-10.1.1/HOL4/src/postkernel/ |
| H A D | Theory.sml | 514 * constants been re-declared after it was built? A constant is
|