/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | KnuthBendixOrder.sml | 38 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 D | Formula.sml | 561 | (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 D | KnuthBendixOrder.sml | 38 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 D | Formula.sml | 561 | (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 D | ACF.sml | 117 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 D | regAllocTest.sml | 56 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 D | fc_examples.sml | 36 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 D | SALScript.sml | 23 `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 D | more_listScript.sml | 115 |- !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 D | LTLScript.sml | 70 (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 D | PropertiesScript.sml | 381 [`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 D | finite_mapLib.sml | 45 val f2 = (rand o rator) c value 58 val imp_thm_inst = ISPECL [f1,f2, ks, k, v] imp_thm
|
H A D | alistScript.sml | 194 ``!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 D | readerMonadScript.sml | 14 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 D | selftest.sml | 49 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 D | pattern_matchingScript.sml | 22 val _ = def "f2" 23 `(f2 0 = 1)`;
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | inst_logic.py | 184 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 D | ClockedSemanticsScript.sml | 165 (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 D | RewritesPropertiesScript.sml | 177 [`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 D | linux64.S | 118 lfd %f2, -32-(20*8)(%r28) 167 stfd %f2, 8(%r30) 177 stfd %f2, 8(%r30) 188 stfs %f2, 4(%r30)
|
H A D | aix_closure.S | 61 .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 D | temporalLib.sml | 181 | 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 D | quotient_pairScript.sml | 278 !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 D | FunctionalRecordUpdate.sml | 7 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 D | v9.S | 61 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
|