/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | CFL_RulesScript.sml | 322 `!ir1 ir2 pre_p1 post_p1 post_p2 stk_f in_f1 f1 f2 out_f1 out_f2. 324 PSPEC ir1 (pre_p1,post_p1) stk_f (in_f1,f1,out_f1) /\ PSPEC ir2 (post_p1,post_p2) stk_f (out_f1,f2,out_f2) 326 PSPEC (SC ir1 ir2) (pre_p1,post_p2) stk_f (in_f1,f2 o f1,out_f2)`, 334 `!cond ir_t ir_f pre_p post_p stk_f cond_f in_f f1 f2 out_f. 337 PSPEC ir_f (pre_p, post_p) stk_f (in_f,f2,out_f) /\ (!st. cond_f (in_f st) = eval_il_cond cond st) 339 PSPEC (CJ cond ir_t ir_f) (pre_p,post_p) stk_f (in_f, (\v.if cond_f v then f1 v else f2 v), out_f)`, 520 `!ir1 ir2 pre_p1 post_p1 post_p2 stk vi1 f1 vo1 f2 vo2. 522 VSPEC ir1 (pre_p1,post_p1) stk (vi1,f1,vo1) /\ VSPEC ir2 (post_p1,post_p2) stk (vo1,f2,vo2) 524 VSPEC (SC ir1 ir2) (pre_p1,post_p2) stk (vi1,f2 o f1,vo2)`, 531 `!cond ir_t ir_f pre_p post_p stk cond_f iv f1 f2 o [all...] |
/seL4-l4v-10.1.1/HOL4/src/datatype/inftree/ |
H A D | inftreeScript.sml | 66 ((iNd b1 f1 = iNd b2 f2 : ('a,'b,'c)inftree) = (b1 = b2) /\ (f1 = f2))``, 78 Q_TAC SUFF_TAC `from_inftree (f1 x) = from_inftree (f2 x)`
|
/seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
H A D | quotient_optionScript.sml | 243 !a1 a2 f1 f2. 244 (R1 ===> R2) f1 f2 /\ (OPTION_REL R1) a1 a2 ==> 245 (OPTION_REL R2) (OPTION_MAP f1 a1) (OPTION_MAP f2 a2)���),
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/ |
H A D | ibmLib.sml | 390 (!f1 f1' f2 f2'. 392 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f2 f2' ==> 393 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE (F_AND (f1, f2)) (F_AND (f1', f2'))) /\ 398 (!f1 f1' f2 f2'. 400 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f2 f2' [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/ |
H A D | inlineCompile.sml | 94 val f2 = mk_pabs(args,rand t2) value 96 (Term`TOTAL(^fb,^f1,^f2)`, 234 val (f2,f3) = dest_pair f2f3 value 237 val f2th = Convert_CONV f2 245 val f2' = (snd o dest_eq o concl) (inline f2th) 248 in prove(``^(concl totalth) = TOTAL( ^f1', ^f2' ,^f3')``,
|
H A D | compile.sml | 62 (* Make an application TOTAL f1 f2 f3 *) 119 (`!f1 f2 f3. Seq (Par f1 f2) f3 = \x. let v = f2 x in f3 (f1 x,v)`, 123 (`!f2 f3. Seq (Par (\x.x) f2) f3 = \x. let v = f2 x in f3 (x,v)`, 144 val f2 = mk_pabs(args,t2) value 146 val th2 = PBETA_CONV (mk_comb(f2,args)) 147 val th3 = ISPECL [f1,f2] Par_de 171 val f2 = mk_pabs(args,t2) value 202 val f2 = mk_pabs(mk_pair(args,v),N) value 220 val f2 = mk_pabs(args,M) value 242 val f2 = mk_pabs(args,t2) value 386 val f2 = mk_pabs(args,rand t2) value 436 val f2 = mk_pabs(args,rand t2) value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | progScript.sml | 294 ``!f1 (f2:'a->'b) g p res res' c m. 296 (!x y. ~g x /\ p x /\ (y = f2 x) ==> SPEC m (res x) c (res' y)) ==> 297 (!x. TAILREC_PRE f1 g p x ==> SPEC m (res x) c (res' (TAILREC f1 f2 g x)))``, 302 ``!f1 (f2:'a->'b) g p res res' c m. 304 (!z x y. ~g x /\ p x /\ (y = f2 x) ==> SPEC m (res z x) c (res' z y)) ==> 305 (!z x. TAILREC_PRE f1 g p x ==> SPEC m (res z x) c (res' z (TAILREC f1 f2 g x)))``,
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/ |
H A D | grammarScript.sml | 324 rw[] >> qabbrev_tac `f2 = snils ++ fss` >> 325 `MAP ptree_fringe ptl = f1 ++ [xp ++ [x]] ++ f2` by simp[Abbr`f2`] >> 331 f2 = MAP ptree_fringe pt2 ��� 336 `FLAT f2 = FLAT fss` by simp[Abbr`f2`, rich_listTheory.FLAT_APPEND] >> 340 disch_then (qxchl [`f1`, `f2`, `fpx`, `fs`] strip_assume_tac) >> 350 f2 = MAP ptree_fringe pt2 ���
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | tripleScript.sml | 26 case_sum f1 f2 x = case x of INL y => f1 y | INR y => f2 y`
|
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | PEGParse.sml | 53 | choice(e1,e2,f1,f2) => pe e1 inp stk (appf1(f1,k)) (returnTo(inp,stk,ksym(e2,appf1(f2,k),fk)))
|
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | Dep.sml | 118 fun pp_couple (f1,f2) (a1,a2) = 121 f2 a2; add_string ")";
|
/seL4-l4v-10.1.1/HOL4/tools/ |
H A D | buildutils.sig | 39 (* [check_against f1 f2] checks to see if file f1 is older than file f2
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | stack_logic.py | 694 fun_offs[f] = max ([offs for (f2, offs) in fcall_offs 695 if f2 == f]) 846 fs = set.union (set ([f for f in graph if [f2 for f2 in graph[f] 847 if f2 in fs2]]), 848 set ([f2 for f in fs2 for f2 in graph[f]]), fs2) 850 entries = list (fs - set ([f2 for f in graph for f2 in graph[f]])) 867 if [f2 fo [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/ |
H A D | encap1.lisp | 34 (defun f2 (x)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/test/ |
H A D | backend_test.sml | 18 f2 = \x. if x = (0w:word32) then x
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | boolLib.sml | 203 (COMB(f1,x1), COMB (f2,x2)) => 204 if aconv f1 f2 then recurse (pRight :: p) x1 x2 205 else if aconv x1 x2 then recurse (pLeft :: p) f1 f2 206 else recurse (pLeft :: p) f1 f2 @ recurse (pRight :: p) x1 x2
|
/seL4-l4v-10.1.1/HOL4/src/combin/ |
H A D | combinScript.sml | 213 `!f1 f2 a b c. ~(b = c) ==> ~((a =+ b) f = (a =+ c) f)`, 234 `!f1 f2 a b c. 235 ((a =+ b) f1 = (a =+ c) f2) ==> 236 (b = c) /\ !v. (a =+ v) f1 = (a =+ v) f2`,
|
/seL4-l4v-10.1.1/HOL4/examples/unification/triangular/nominal/ |
H A D | nunifDefScript.sml | 157 Q.ABBREV_TAC `f2 = \n. FST (SND (f n))` THEN 158 `!n. FST (SND (f n)) = f2 n` by SRW_TAC [][Abbr`f2`] THEN 164 sysvars (f1 n) (f2 n) (f3 n) ��� sysvars (f1 m) (f2 m) (f3 m)` 181 (sysvars (f1 n) (f2 n) (f3 n) = sysvars (f1 m) (f2 m) (f3 m))` 185 sysvars (f1 (f' m)) (f2 (f' m)) (f3 (f' m)) 187 sysvars (f1 m) (f2 m) (f3 m)` 190 (sysvars (f1 (f' m)) (f2 ( [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/encap/ |
H A D | example.lisp | 32 (defun f2 (x)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/mips/ |
H A D | n32.S | 249 s.d $f2, 8(t4) 257 s.s $f2, 4(t4) 265 s.s $f2, 8(t4) 273 s.d $f2, 8(t4) 376 3 - return value high (v1 or $f2) 483 l.d $f2, V1_OFF2($sp) 489 l.s $f2, V1_OFF2($sp) 495 l.s $f2, V1_OFF2($sp) 501 l.d $f2, V1_OFF2($sp)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/ |
H A D | sysv.S | 90 lfd %f2,-16-(8*4)-(7*8)(%r28) 137 stfd %f2,8(%r30)
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Subst.sml | 213 | matchList sub ((Term.Fn (f1,args1), Term.Fn (f2,args2)) :: rest) = 214 if Name.equal f1 f2 andalso length args1 = length args2 then 240 | solve' sub (Term.Fn (f1,args1)) (Term.Fn (f2,args2)) rest = 241 if Name.equal f1 f2 andalso length args1 = length args2 then
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Subst.sml | 213 | matchList sub ((Term.Fn (f1,args1), Term.Fn (f2,args2)) :: rest) = 214 if Name.equal f1 f2 andalso length args1 = length args2 then 240 | solve' sub (Term.Fn (f1,args1)) (Term.Fn (f2,args2)) rest = 241 if Name.equal f1 f2 andalso length args1 = length args2 then
|
/seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/src/ |
H A D | decidable_separationLogicLibScript.sml | 572 ``!f1 f2 C pf sf pf' sf'. 574 LIST_DS_ENTAILS C (SAFE_MAP F f1 PF_TURN_EQ pf, sf) (SAFE_MAP F f2 PF_TURN_EQ pf', sf')``, 866 (SF_TRIVIAL_FILTER_PRED (sf_bin_tree (f1,f2) e) = (e = dse_nil)) /\ 961 ``!f1 f2 f3 f4 f5 c1 c2 pfL sfL pfL' sfL'. 963 LIST_DS_ENTAILS (c1, (POS_FILTER f1 (\x. (FST x = SND x)) c2)) (POS_FILTER f2 PF_TRIVIAL_FILTER_PRED pfL, POS_FILTER f3 SF_TRIVIAL_FILTER_PRED sfL) (POS_FILTER f4 PF_TRIVIAL_FILTER_PRED pfL',POS_FILTER f5 SF_TRIVIAL_FILTER_PRED sfL')``, 1255 ``!f1 f2 c1 c2 pfL sfL pfL' sfL'. 1257 LIST_DS_ENTAILS (c1,c2) (HYPOTHESIS_RULE_MAP c1 [] pfL 0 f1 pfL,sfL) (HYPOTHESIS_RULE_MAP c1 pfL pfL' 0 f2 pfL',sfL')``, 1319 ``!e f1 f2 f1' f2' n m c1 c2 pfL sfL pfL' sfL'. 1320 (((f1' = f1) /\ (f2' [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/src/ |
H A D | riscv.spec | 3204 ; f2 = FPRS(rs2) 3205 ; res = match FP32_Compare(f1, f2) 3208 case FP_GT => f2 3209 case FP_UN => if ( (FP32_IsSignalingNan(f1) or FP32_IsSignalingNan(f2)) 3210 or (f1 == RV32_CanonicalNan and f2 == RV32_CanonicalNan)) 3212 else -- either f1 or f2 should be a quiet NaN 3213 if f1 == RV32_CanonicalNan then f2 else f1 3223 ; f2 = FPRS(rs2) 3224 ; res = match FP32_Compare(f1, f2) 3225 { case FP_LT => f2 [all...] |