Lines Matching defs:f1
102 (`!f1 f2 f3. Seq (Par f1 f2) f3 = \x. let v = f2 x in f3 (f1 x,v)`,
136 val f1 = mk_pabs(args,t1)
138 val th1 = PBETA_CONV (mk_comb(f1,args))
140 val th3 = ISPECL [f1,f2] Par_def
141 val ptm = mk_pabs(args, mk_pair(mk_comb(f1,args),mk_comb(f2,args)))
163 val f1 = mk_pabs(args,t1)
166 val th1 = PBETA_CONV (mk_comb(f1,args))
168 val th3 = ISPECL [fb,f1,f2] Ite_def
171 mk_cond(mk_comb(fb,args),mk_comb(f1,args),mk_comb(f2,args)))
194 val f1 = mk_pabs(args,args)
197 val th1 = ISPECL [f1,f2,f3] LET_SEQ_PAR_THM
214 val f1 = mk_pabs(args,t1)
284 (* RecConvert (|- f x = if f1 x then f2 x else f(f3 x)) *)
285 (* (|- TOTAL(f1,f2,f3)) *)
360 val f1 = mk_pabs(args,t1)
362 val thm = ISPECL[func,fb,f1,f2] Rec_INTRO