| /seL4-l4v-master/HOL4/examples/countable/ |
| H A D | countable_initScript.sml | 58 val (hyps,c) = strip_imp (concl inj) value
|
| H A D | countableLib.sml | 71 val hyps = map (mk_inj_rwt_tm []) (zip (map (fn a => mk_var(dest_vartype a, a)) args) helpers) value
|
| /seL4-l4v-master/HOL4/src/HolSat/ |
| H A D | dpll.sml | 54 val hyps = hypset th value
|
| /seL4-l4v-master/HOL4/examples/ |
| H A D | dpll.sml | 45 val hyps = hypset th value
|
| /seL4-l4v-master/HOL4/src/metis/ |
| H A D | mlibResolution.sml | 115 and hyps = map thm_to_formula hyps value
123 and hyps = map (mlibClause.mk_clause clause_parm) hyps value
140 val (hyps,set) = mlibClauseset.factor hyps set value
[all...] |
| H A D | mlibSolver.sml | [all...] |
| /seL4-l4v-master/HOL4/src/new-datatype/ |
| H A D | Witness.sml | 54 val hyps = (fst o dest_imp o concl) trans value
|
| /seL4-l4v-master/HOL4/src/1/ |
| H A D | resolve_then.sml | 107 val hyps = HOLset.union(hypset th1, hypset th2) value
|
| H A D | Conv.sml | 2496 val (hyps, c) = dest_thm th value
|
| /seL4-l4v-master/HOL4/src/simp/src/ |
| H A D | Cache.sml | [all...] |
| /seL4-l4v-master/HOL4/src/coretypes/ |
| H A D | DefnBase.sml | 44 fun hyps thl = HOLset.listItems function
|
| /seL4-l4v-master/HOL4/src/IndDef/ |
| H A D | IndDefRules.sml | 315 val hyps = strip_conj(snd(strip_exists ant)) value
|
| /seL4-l4v-master/HOL4/src/quotient/examples/ |
| H A D | tactics.sml | 432 val (hyps,body) = strip_imp imps; value
440 val (hyps,body) = strip_imp imps in value
|
| H A D | ind_rel.sml | 649 val hyps = if is_an_imp then strip_conj hyp2 else [] value
1366 val hyps = map (rand o rator) new_imps value
[all...] |
| /seL4-l4v-master/HOL4/src/meson/src/ |
| H A D | mesonLib.sml | 468 let val ((hyps,conc),tag) = rule value
|
| /seL4-l4v-master/HOL4/src/probability/ |
| H A D | hurdUtils.sig | 269 val hyps : thm list -> term list value
|
| H A D | hurdUtils.sml | 725 val hyps = foldl (fn (h,t) => tunion (hyp h) t) []; value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/ |
| H A D | mechReasoning.sml | 1730 val hyps = hyp hyp_thm; value
|
| /seL4-l4v-master/HOL4/examples/acl2/ml/ |
| H A D | encodeLib.sml | 1041 val hyps = map (mk_fix_id_conc target) (set_diff tvs [t]) value
|
| H A D | functionEncodeLib.sml | 1009 let val hyps = hyp thm value
|
| H A D | polytypicLib.sml | 3324 val (hyps,conc) = (strip_conj ## strip_conj) (dest_imp_only (snd (strip_forall (concl result)))) value
|
| /seL4-l4v-master/HOL4/src/datatype/ |
| H A D | ind_types.sml | 1204 let val hyps = hyp th value
|
| /seL4-l4v-master/HOL4/src/quotient/src/ |
| H A D | quotient.sml | 1784 val hyps = map (fn (x,y) => list_mk_comb (tyREL (type_of x), [x,y])) value
2246 val hyps = map (fn (x,y) => list_mk_comb (tyREL (type_of x), [x,y])) value
|
| /seL4-l4v-master/HOL4/src/tfl/src/ |
| H A D | Defn.sml | |