Searched refs:compressed (Results 1 - 8 of 8) sorted by relevance
| /seL4-l4v-master/isabelle/src/Pure/Thy/ |
| H A D | export.scala | 4 Manage theory exports: compressed blobs.
30 val compressed = SQL.Column.bool("compressed")
35 List(session_name, theory_name, name, executable, compressed, body))
98 val (compressed, bytes) = body.join
99 if (compressed) bytes.uncompress(cache = cache) else bytes
107 val (compressed, bytes) = body.join
114 stmt.bool(5) = compressed
158 Data.table.select(List(Data.executable, Data.compressed, Data.body),
165 val compressed
[all...] |
| /seL4-l4v-master/l4v/isabelle/src/Pure/Thy/ |
| H A D | export.scala | 4 Manage theory exports: compressed blobs.
30 val compressed = SQL.Column.bool("compressed")
35 List(session_name, theory_name, name, executable, compressed, body))
98 val (compressed, bytes) = body.join
99 if (compressed) bytes.uncompress(cache = cache) else bytes
107 val (compressed, bytes) = body.join
114 stmt.bool(5) = compressed
158 Data.table.select(List(Data.executable, Data.compressed, Data.body),
165 val compressed
[all...] |
| /seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | Main.C | 286 Proof compressed; local
287 S.proof->compress(compressed,S.proof->last());
289 reportf("Checking compressed proof...\n"),
290 checkProof(&compressed);
291 if (proof != NULL) compressed.save(proof);
|
| /seL4-l4v-master/isabelle/src/Pure/General/ |
| H A D | bytes.scala | 213 val compressed = compress(options = options, cache = cache)
214 if (compressed.length < length) (true, compressed) else (false, this)
|
| /seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
| H A D | bytes.scala | 213 val compressed = compress(options = options, cache = cache)
214 if (compressed.length < length) (true, compressed) else (false, this)
|
| /seL4-l4v-master/HOL4/src/HolSmt/ |
| H A D | Z3_Proof.sml | 24 in the generated proofs. Rules that only appear in compressed Z3
|
| /seL4-l4v-master/HOL4/tools/Holmake/ |
| H A D | internal_functions.sig | 51 TABs between tokens in sl will have been compressed into just one
|
| /seL4-l4v-master/HOL4/examples/formal-languages/regular/ |
| H A D | Regexp_Type.sml | 162 (* compressed version of ranged. Not used since it is hard for derivative *)
|
Completed in 76 milliseconds