| /seL4-l4v-10.1.1/HOL4/src/rational/ |
| H A D | intExtensionLib.sig | 5 type goal = Abbrev.goal type
|
| H A D | fracUtils.sig | 5 type goal = Abbrev.goal type
|
| H A D | ratUtils.sig | 5 type goal = Abbrev.goal type
|
| H A D | fracLib.sig | 5 type goal = Abbrev.goal type
|
| H A D | jbUtils.sig | 5 type goal = Abbrev.goal type
|
| H A D | ratLib.sig | 5 type goal = Abbrev.goal type
|
| H A D | schneiderUtils.sig | 5 type goal = Abbrev.goal type
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/bytecode/ |
| H A D | lisp_alt_semanticsScript.sml | 202 val goal = lemma |> concl |> rand; value
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/soundness-thm/ |
| H A D | milawa_soundnessScript.sml | 43 val goal = mk_imp(assum,assum2) value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Abbrev.sig | 8 type goal = term list * term type
|
| H A D | Abbrev.sml | 8 type goal = term list * term type
|
| /seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
| H A D | selftest.sml | 39 val goal = ``1 < foo`` value
174 val goal = ([���c3 < x���, ���x < 3���], ���p:bool���) value
|
| /seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
| H A D | tttThmData.sml | 50 val goal = dest_thm thm value
|
| /seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
| H A D | Z3.sml | 39 val (goal, _) = SolverSpec.simplify (SmtLib.SIMP_TAC false) goal value
79 val (goal, validation) = SolverSpec.simplify (SmtLib.SIMP_TAC true) goal value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/boss/ |
| H A D | selftest.sml | 42 val goal = ([] : term list, ``(n + 10) * y <= 42315 /\ !x y:'a. x < f y``) value
57 val goal = ([``x = 3``, ``FACT n = 10``], ``n + x = 7``) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/ |
| H A D | arm_cheney_allocScript.sml | 409 val goal = (fst o dest_imp o concl) th value
436 val goal = (fst o dest_imp o concl) th value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/ |
| H A D | jit_codegenScript.sml | 614 val goal = mk_imp(tm,tm2) value
|
| /seL4-l4v-10.1.1/HOL4/examples/miller/formalize/ |
| H A D | numContext.sml | 180 val goal = subst [(x |-> modulus)] target value
217 val goal = subst [(x |-> modulus)] target value
|
| /seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | Proof.C | 255 void Proof::compress(Proof& dst, ClauseId goal) argument
364 void Proof::traverse(ProofTraverser& trav, int& res_count, ClauseId goal) argument
378 fout << "G " << goal << "\n"; local
|
| /seL4-l4v-10.1.1/HOL4/src/q/ |
| H A D | selftest.sml | 13 val goal = ``?a:'c b:'d. Q a b`` value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/acl2/ |
| H A D | m1_progLib.sml | 91 val goal = mk_eq(new_lhs,tm3) value
107 val goal = mk_eq (tm1,tm9) value
125 val goal = mk_eq(tm10,tm12) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | func_decompileLib.sml | 91 val goal = th |> concl |> dest_imp |> fst value
138 val goal = th |> concl |> dest_imp |> fst value
178 val goal = th |> concl |> dest_imp |> fst value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ |
| H A D | ppc_Lib.sml | 209 val goal = mk_imp(tm2,tm) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
| H A D | x86_Lib.sml | 277 val goal = mk_imp(tm2,tm) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
| H A D | x64_Lib.sml | 266 val goal = mk_imp(tm2,tm) value
|