Searched defs:proofs (Results 1 - 14 of 14) sorted by relevance
| /seL4-l4v-10.1.1/HOL4/examples/imperative/ |
| H A D | necec2010.sml | 28 Following this, flags can be set to tailor the environment to the users liking. In the case of this file, to get feedback about data types and proofs, structure
|
| /seL4-l4v-10.1.1/HOL4/src/proofman/ |
| H A D | Manager.sig | 9 datatype proofs = PRFS of proof list type
[all...] |
| H A D | proofManagerLib.sig | 5 type proofs = Manager.proofs type
[all...] |
| H A D | Manager.sml | 25 datatype proofs = PRFS of proof list; type
|
| H A D | proofManagerLib.sml | 13 type proofs = Manager.proofs type
20 fun proofs() = !the_proofs; function
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
| H A D | Defn.sig | 6 type proofs = Manager.proofs type
|
| H A D | Defn.sml | 8 type proofs = Manager.proofs type
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/poly/ |
| H A D | holfoot_command_line.sml | 103 val proofs = proofManagerLib.status () value
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Intro/document/ |
| H A D | getting.tex | |
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Intro/document/ |
| H A D | getting.tex | |
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | mechReasoning.sml | 499 val proofs = append_proofs [th_proof, unchanged_thm_proof, used_stack_thm_proof, spec_thm_proof] value
1217 val proofs = append_proofs [proofs, f_th_proof, unchanged_th_proof, well_formed_th_proof, th_proof] value
[all...] |
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Tptp.sml | 2537 val (proofs,(names,fofs,defs)) = value
2551 val (proofs,(formulas,_)) = value
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Tptp.sml | 2537 val (proofs,(names,fofs,defs)) = value
2551 val (proofs,(formulas,_)) = value
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | polytypicLib.sml | 3192 val proofs = value
3354 val (proofs,thm') = prove_all_split_terms (get_ind,get_def,conv,create_conv,dead_thm,dead_value) matches thm handle e => wrap e value
3608 val proofs = map (fn (t,(assums:term list,goal:term)) => value
[all...] |
Completed in 261 milliseconds