Searched defs:ants (Results 1 - 8 of 8) sorted by relevance

/seL4-l4v-10.1.1/HOL4/src/1/
H A Ddep_rewrite.sml250 val (ants,conseq) = strip_imp_only bod value
H A DDrule.sml801 let val (ants, uth) = strip_gen_left (UNDISCH_TM o SPEC_ALL) th ; value
/seL4-l4v-10.1.1/HOL4/src/IndDef/
H A DCoIndDefLib.sml22 val (ants, concs) = split (map dest_imp bodies) value
H A DIndDefRules.sml142 val ants = strip_conj (#1 (dest_imp (concl ith))) value
H A DInductiveDefinition.sml281 val (ants,concs) = split(map dest_imp bodies) value
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DRW.sml108 let val (ants,(lhs,rhs)) = (I##dest_eq)(strip_imp_only(concl th)) value
207 let val (ants,eq) = strip_imp_only (concl th) value
649 val ants = strip_conj (fst(dest_imp (concl icong))) value
H A DDefn.sml797 val (ants,Pa) = strip_imp_only tm value
/seL4-l4v-10.1.1/HOL4/src/quotient/src/
H A Dquotient.sml130 let val ants = get_ants (concl th) value
3601 val (ants, base) = if is_imp body then value
3986 val ants = if ant=T then [] else strip_conj ant value
[all...]

Completed in 133 milliseconds