| /seL4-l4v-10.1.1/HOL4/src/pred_set/src/ |
| H A D | PSet_ind.sml | 44 val (ant,conseq) = dest_imp Body value
60 val (ant,conseq) = dest_imp Body value
|
| /seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
| H A D | wfrecUtils.sml | 52 let val (ant,conseq) = dest_imp_only tm value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Mutual.sml | 362 val (ant,conseq) = dest_imp(concl spec) value
|
| H A D | Thm_cont.sml | 191 val (ant, conseq) = dest_imp w value
|
| H A D | selftest.sml | 228 val ant = let value
|
| H A D | dep_rewrite.sml | 174 let val (ant,conseq) = dest_thm th value
|
| H A D | Tactical.sml | 649 val (ant, conseq) = dest_imp w value
|
| /seL4-l4v-10.1.1/HOL4/src/simp/src/ |
| H A D | Unwind.sml | 531 let val (ant,value) = find_var_value (hd vars) (strip_univ body) value
|
| H A D | Cond_rewr.sml | 401 val (ant,c) = dest_imp w value
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/lambda/ |
| H A D | etaScript.sml | 65 val {ant,conseq} = dest_imp Body value
104 val {ant,conseq} = dest_imp Body value
|
| H A D | betaScript.sml | 63 val {ant,conseq} = dest_imp Body value
1551 val {ant,conseq} = dest_imp Body value
|
| H A D | reductionScript.sml | 56 val {ant,conseq} = dest_imp Body value
242 val {ant,conseq} = dest_imp Body value
|
| /seL4-l4v-10.1.1/HOL4/src/IndDef/ |
| H A D | CoIndDefLib.sml | 39 let val ant = fst (dest_imp (concl th)) value
|
| H A D | IndDefRules.sml | 314 then let val (ant,_) = dest_imp bdy value
345 let val (ant,conseq) = dest_imp stm value
437 in let val (ant,conseq) = dest_imp rule value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/coretypes/ |
| H A D | pairTools.sml | 209 let val (ant,conseq) = dest_imp(concl thm) value
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
| H A D | Recftn.sml | 572 val ant = mk_conj {conj1 = conj1, conj2 = conj2} value
|
| H A D | ConsThms.sml | 530 val {ant, conseq} = dest_imp rest_of_term value
|
| /seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
| H A D | numSimps.sml | 524 val ant = #1 (dest_imp (concl th)) value
545 val (ant, w) = strip_imp (concl th) value
570 val (ant, w) = strip_imp (concl th) value
|
| /seL4-l4v-10.1.1/HOL4/src/num/ |
| H A D | numLib.sml | 138 val (ant,_) = dest_imp Body value
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/ |
| H A D | semanticsScript.sml | 73 val {ant,conseq} = dest_imp Body value
1786 val {ant,conseq} = dest_imp Body value
|
| H A D | reductionScript.sml | 296 val {ant,conseq} = dest_imp Body value
|
| /seL4-l4v-10.1.1/HOL4/src/temporal/src/ |
| H A D | temporalLib.sml | |
| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/ |
| H A D | tactics.sml | 95 let val (ant,conseq) = dest_thm th value
209 let val (ant,cns) = dest_imp(concl imp_th) in value
220 let val (ant,cns) = dest_imp gl in value
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | lzConv.sml | 1090 val {ant,conseq} = dest_imp Body handle HOL_ERR _ => raise FI_ERR value
1120 let val {ant, ...} = dest_imp tm value
1140 let val {ant,conseq} = dest_imp tm value
1168 val {ant = P,conseq = Q} = dest_imp Body handle HOL_ERR _ => raise EI_ERR value
1231 let val {ant,conseq} = dest_imp tm value
1263 let val {ant,conseq} = dest_imp tm value
1489 let val {ant,conseq} = dest_imp tm value
1510 let val {ant,conseq} = dest_imp tm value
1601 let val {ant,conseq} = dest_imp imp value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
| H A D | quotient.sml | 121 let val {ant,conseq} = (dest_imp o snd o strip_forall) tm value
155 val ant = (#ant o dest_imp o snd o strip_forall o concl) imp1 value
613 val {ant, conseq} = Rsyntax.dest_imp body value
651 val {ant, conse value
2481 let val {ant, conseq} = dest_imp tm value
3602 let val {ant, conseq} = Rsyntax.dest_imp body value
3984 val (ant,conseq) = if is_imp body andalso not (is_neg body) value
[all...] |