Searched refs:f2 (Results 76 - 100 of 315) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DKnuthBendixOrder.sml38 fn ((f1,n1),(f2,n2)) =>
41 | EQUAL => Name.compare (f1,f2)
153 and precedenceLess (Term.Fn (f1,a1)) (Term.Fn (f2,a2)) =
154 (case precedence ((f1, length a1), (f2, length a2)) of
172 and precedenceCmp (Term.Fn (f1,a1)) (Term.Fn (f2,a2)) =
173 (case precedence ((f1, length a1), (f2, length a2)) of
H A DFormula.sml561 | (true, And (f1,f2)) => split asms true f1 @ split (f1 :: asms) true f2
562 | (true, Or (f1,f2)) => split (Not f1 :: asms) true f2
563 | (true, Imp (f1,f2)) => split (f1 :: asms) true f2
564 | (true, Iff (f1,f2)) =>
565 split (f1 :: asms) true f2 @ split (f2 :: asms) true f1
570 | (false, And (f1,f2))
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DKnuthBendixOrder.sml38 fn ((f1,n1),(f2,n2)) =>
41 | EQUAL => Name.compare (f1,f2)
153 and precedenceLess (Term.Fn (f1,a1)) (Term.Fn (f2,a2)) =
154 (case precedence ((f1, length a1), (f2, length a2)) of
172 and precedenceCmp (Term.Fn (f1,a1)) (Term.Fn (f2,a2)) =
173 (case precedence ((f1, length a1), (f2, length a2)) of
H A DFormula.sml561 | (true, And (f1,f2)) => split asms true f1 @ split (f1 :: asms) true f2
562 | (true, Or (f1,f2)) => split (Not f1 :: asms) true f2
563 | (true, Imp (f1,f2)) => split (f1 :: asms) true f2
564 | (true, Iff (f1,f2)) =>
565 split (f1 :: asms) true f2 @ split (f2 :: asms) true f1
570 | (false, And (f1,f2))
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A DACF.sml117 val f2 = mk_pabs(args,t2) value
120 val th2 = PBETA_CONV (mk_comb(f2,args))
121 val th3 = ISPECL [fb,f1,f2] cj_def
124 mk_cond(mk_comb(fb,args),mk_comb(f1,args),mk_comb(f2,args)))
150 val f2 = mk_pabs(v, N) value
152 ISPECL [f1,f2] sc_def
159 val f2 = mk_pabs(args1,N) value
161 ISPECL [f1,f2] sc_def
231 (* tr_convert (|- f x = if f1 x then f2 x else f(f3 x)) *)
232 (* (|- TOTAL(f1,f2,f
271 val f2 = mk_pabs(args,rand t2) value
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/test/
H A DregAllocTest.sml56 f2 = \(v1,v2,v3:word32).
80 let (v3,v4) = f2 (v1,v2,v3) in
87 let (v3,v4) = f2 (v1,v1,v1) in
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/examples/
H A Dfc_examples.sml36 val def2 = Define `f2 x = x * f1 x`;
67 f2 (st<MR R0>)))
71 Name : f2
85 Name : f2
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/
H A DSALScript.sml23 `tr (x:'a) = if f1 x then x else tr (f2 x)`;
29 `!f f1 f2.
30 (!x:'a. f x = if f1(x) then x else f(f2 x))
31 ==> (?R. WF R /\ (!x. ~f1 x ==> R (f2 x) x))
32 ==> (f:'a->'a = tr f1 f2)`,
45 `!f f1 f2 f3.
46 (!x:'a. f x = if f1(x) then f2(x) else f(f3 x))
48 ==> (f:'a->'b x = let y = (tr f1 f3) x in f2 y)`,
53 Q.SPEC `\x. f x = let y = (tr f1 f3) x in f2 y`) THEN
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/
H A Dmore_listScript.sml115 |- !f1 f2 l. FILTER f1 (MAP f2 l) = MAP f2 (FILTER (f1 o f2) l)
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A DLTLScript.sml70 (Atoms (AND f1 f2) = Atoms f1 UNION Atoms f2)
72 (Atoms (OR f1 f2) = Atoms f1 UNION Atoms f2)
80 (Atoms (UNTIL f1 f2) = Atoms f1 UNION Atoms f2)
82 (Atoms (WEAK_UNTIL f1 f2) = Atoms f1 UNION Atoms f2)`;
196 (SEM M p (AND f1 f2) = SEM M p f1 /\ SEM M p f2)
[all...]
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/official-semantics/
H A DPropertiesScript.sml381 [`P`,`\ (r,f). P f`,`\ (f,b). P f`,`\ (f1,f2). P f1 /\ P f2`]
404 (F_CLOCK_FREE (F_AND(f1,f2)) = F_CLOCK_FREE f1 /\ F_CLOCK_FREE f2)
408 (F_CLOCK_FREE (F_UNTIL(f1,f2)) = F_CLOCK_FREE f1 /\ F_CLOCK_FREE f2)
440 (* 3. F_AND (f1,f2) *)
454 (* 5. F_UNTIL(f1,f2) f *)
524 * Formula disjunction: f1 \/ f2
529 ``UF_SEM p (F_OR(f1,f2))
[all...]
/seL4-l4v-10.1.1/HOL4/src/finite_map/
H A Dfinite_mapLib.sml45 val f2 = (rand o rator) c value
58 val imp_thm_inst = ISPECL [f1,f2, ks, k, v] imp_thm
H A DalistScript.sml194 ``!f1 f2 al. INJ f1 (set (MAP FST al)) UNIV ==>
195 (alist_to_fmap (MAP (\ (x,y). (f1 x, f2 y)) al) =
196 MAP_KEYS f1 (f2 o_f alist_to_fmap al))``,
238 Q.MATCH_ABBREV_TAC `MAP f2 al = al` THEN
239 Q_TAC SUFF_TAC `!x. MEM x al ==> (f1 x = f2 x)` THEN1 PROVE_TAC[MAP_EQ_f] THEN
240 SRW_TAC[][Abbr`f1`,Abbr`f2`] THEN
325 qmatch_abbrev_tac `ALL_DISTINCT (MAP f2 ls)` >>
326 qsuff_tac `MAP f2 ls = MAP f1 ls` >- rw[] >>
327 rw[MAP_EQ_f,Abbr`f1`,Abbr`f2`,Abbr`ls`,DOMSUB_FAPPLY_THM])
332 ``!f1 f2
[all...]
/seL4-l4v-10.1.1/HOL4/src/monad/more_monads/
H A DreaderMonadScript.sml14 MCOMPOSE (f1 : 'a -> ('s -> 'b)) (f2 : 'b -> ('s -> 'c)) a = BIND (f1 a) f2
/seL4-l4v-10.1.1/HOL4/src/num/termination/
H A Dselftest.sml49 f2 (y : 'a) = \x. case x of 0 => 0n | SUC n => f2 y n
/seL4-l4v-10.1.1/HOL4/src/tfl/src/test/
H A Dpattern_matchingScript.sml22 val _ = def "f2"
23 `(f2 0 = 1)`;
/seL4-l4v-10.1.1/graph-refine/
H A Dinst_logic.py184 for f2 in functions[f].function_calls ():
185 if "instruction'" not in f2:
187 if functions[f2].entry:
190 unhandled[f].append (f2)
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/
H A DClockedSemanticsScript.sml165 (F_SEM v c (F_AND(f1,f2)) =
166 F_SEM v c f1 /\ F_SEM v c f2)
196 (F_SEM v c (F_UNTIL(f1,f2)) =
199 F_SEM (RESTN v k) c f2 /\
237 (F_SEM v c (F_AND(f1,f2)) =
238 F_SEM v c f1 /\ F_SEM v c f2)
268 (F_SEM v c (F_UNTIL(f1,f2)) =
271 F_SEM (RESTN v k) c f2 /\
H A DRewritesPropertiesScript.sml177 [`P`,`\ (f,b). P f`,`\ (r,f). P f`,`\ (f1,f2). P f1 /\ P f2`]
423 * Formula disjunction: f1 \/ f2
428 ``UF_SEM v (F_OR(f1,f2)) = UF_SEM v f1 \/ UF_SEM v f2``,
432 * Formula conjunction: f1 /\ f2
437 ``UF_SEM v (F_AND(f1,f2)) = UF_SEM v f1 /\ UF_SEM v f2``,
441 * Formula implication: f1 --> f2
446 ``UF_SEM v (F_IMPLIES (f1,f2))
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/
H A Dlinux64.S118 lfd %f2, -32-(20*8)(%r28)
167 stfd %f2, 8(%r30)
177 stfd %f2, 8(%r30)
188 stfs %f2, 4(%r30)
H A Daix_closure.S61 .set f2,2
134 stfd f2, 128+(1*8)(r1)
210 lfd f2, 112+8(r1)
307 stfd f2, 72+(1*8)(r1)
383 lfd f2, 56+8(r1)
/seL4-l4v-10.1.1/HOL4/src/temporal/src/
H A DtemporalLib.sml181 | temporal2hol (conj(f1,f2)) =
184 val t2 = temporal2hol f2
187 | temporal2hol (disj(f1,f2)) =
190 val t2 = temporal2hol f2
193 | temporal2hol (imp(f1,f2)) =
196 val t2 = temporal2hol f2
199 | temporal2hol (equ(f1,f2)) =
202 val t2 = temporal2hol f2
205 | temporal2hol (ifte(f1,f2,f3)) =
208 val t2 = temporal2hol f2
[all...]
/seL4-l4v-10.1.1/HOL4/src/quotient/src/
H A Dquotient_pairScript.sml278 !f1 f2.
279 ((R1 ### R2) ===> R3) f1 f2 ==>
280 (R1 ===> R2 ===> R3) (CURRY f1) (CURRY f2)���),
320 !f1 f2.
321 (R1 ===> R2 ===> R3) f1 f2 ==>
322 ((R1 ### R2) ===> R3) (UNCURRY f1) (UNCURRY f2)���),
358 !f1 f2 g1 g2.
359 (R1 ===> R2) f1 f2 /\ (R3 ===> R4) g1 g2 ==>
360 ((R1 ### R3) ===> (R2 ### R4)) (f1 ## g1) (f2 ## g2)���),
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DFunctionalRecordUpdate.sml7 fun f2 z = next f1 z function
8 fun f3 z = next f2 z
33 fun c2 from = c1 (from f2)
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/sparc/
H A Dv9.S61 ldd [%l0+ARGS+8], %f2
108 std %f2, [%i4+8]
120 std %f2, [%i4+40]
160 std %f2, [FP-120]
210 ldd [FP-152], %f2
223 ldd [FP-152], %f2

Completed in 203 milliseconds

1234567891011>>