| /seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | Main.C | 206 bool compress = false; local
229 compress = true;
284 if (compress) { // ...compress, and possibly check
287 S.proof->compress(compressed,S.proof->last());
|
| H A D | Proof.h | 79 void compress (Proof& dst, ClauseId goal = ClauseId_NULL); // 'dst' should be a newly constructed, empty proof.
|
| H A D | Proof.C | 255 void Proof::compress(Proof& dst, ClauseId goal) function in class:Proof
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
| H A D | properties.scala | 49 def compress(ps: List[T],
56 compress(options = options, cache = cache)
|
| H A D | bytes.scala | 202 def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache()): Bytes =
212 val compressed = compress(options = options, cache = cache)
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
| H A D | properties.scala | 49 def compress(ps: List[T],
56 compress(options = options, cache = cache)
|
| H A D | bytes.scala | 202 def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache()): Bytes =
212 val compressed = compress(options = options, cache = cache)
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
| H A D | markup.scala | 579 id: Option[String], serial: Long, theory_name: String, name: String, compress: Boolean)
582 val COMPRESS = "compress"
591 (COMPRESS, Value.Boolean(compress)),
593 Some((Args(None, serial, theory_name, name, compress), isabelle.Path.explode(file)))
605 (COMPRESS, Value.Boolean(compress))) =>
606 Some(Args(proper_string(id), serial, theory_name, name, compress))
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
| H A D | markup.scala | 579 id: Option[String], serial: Long, theory_name: String, name: String, compress: Boolean)
582 val COMPRESS = "compress"
591 (COMPRESS, Value.Boolean(compress)),
593 Some((Args(None, serial, theory_name, name, compress), isabelle.Path.explode(file)))
605 (COMPRESS, Value.Boolean(compress))) =>
606 Some(Args(proper_string(id), serial, theory_name, name, compress))
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/Thy/ |
| H A D | export.scala | 131 if (args.compress) Future.fork(body.maybe_compress(cache = cache))
|
| H A D | sessions.scala | 1187 stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = xz_cache)
1188 stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = xz_cache)
1189 stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = xz_cache)
1190 stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = xz_cache)
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/ |
| H A D | export.scala | 131 if (args.compress) Future.fork(body.maybe_compress(cache = cache))
|
| H A D | sessions.scala | 1187 stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = xz_cache)
1188 stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = xz_cache)
1189 stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = xz_cache)
1190 stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = xz_cache)
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/Admin/ |
| H A D | build_log.scala | 682 compress(cache = cache))
1058 { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = xz_cache).proper) },
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/ |
| H A D | build_log.scala | 682 compress(cache = cache))
1058 { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = xz_cache).proper) },
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/tests/round-trip/gold/ |
| H A D | axioms.lisp | 3258 '"Attempted to compress a one-dimensional array named ~
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Sledgehammer/document/ |
| H A D | root.tex | 330 \textit{compress} (\S\ref{output-format}).
1244 \opdefault{compress}{int}{smart}
1253 Alias for ``\textit{compress} = 1''.
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Sledgehammer/document/ |
| H A D | root.tex | 330 \textit{compress} (\S\ref{output-format}).
1244 \opdefault{compress}{int}{smart}
1253 Alias for ``\textit{compress} = 1''.
|
| /seL4-l4v-10.1.1/HOL4/polyml/ |
| H A D | Makefile.in | 900 "legacy program 'compress' is deprecated." >&2
902 tardir=$(distdir) && $(am__tar) | compress -c >$(distdir).tar.Z
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
| H A D | Makefile.in | 1590 "legacy program 'compress' is deprecated." >&2
1592 tardir=$(distdir) && $(am__tar) | compress -c >$(distdir).tar.Z
|