/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Term.sml | 128 | (Fn (f1,a1), Fn (f2,a2)) => 129 (case Name.compare (f1,f2) of
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Term.sml | 128 | (Fn (f1,a1), Fn (f2,a2)) => 129 (case Name.compare (f1,f2) of
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/64/ |
H A D | traps.S | 437 INT_HANDLER_WITHOUT_ERR_CODE(f2,0)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | mechReasoning.sml | 406 val (ir2,(pre_p2,post_p2),stk_f,(ins2,f2,outs2)) = get_spec_info (hd specL2); 416 val sc_f = combinSyntax.mk_o (f2,f1); 669 val (ir2,(pre_p2,post_p2),stk_f,(ins2,f2,outs2)) = get_spec_info (hd specL2); 681 [mk_comb(cj_cond,initV), mk_comb(f1,initV), mk_comb(f2,initV)]));
|
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | Lexis.sml | 265 `tmvar_vary' can be used to generate f, f0, f1, f2, f3 ...
|
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/ |
H A D | generalHelpersScript.sml | 679 ``!l1 l2 l3 l4 f1 f2 s. 681 (FOLDR (��a sofar. f2 a ��� sofar) s (l1++l2)) (l3++l4)) 683 (FOLDR (��a sofar. f2 a ��� sofar) s l1) l3) 685 (FOLDR (��a sofar. f2 a ��� sofar) s l2) l4)))``,
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | acl2encodeLib.sml | 1386 fun mapff f1 f2 [] = [] 1387 | mapff f1 f2 (x::xs) = f1 x :: f2 x:: mapff f1 f2 xs;
|
/seL4-l4v-10.1.1/HOL4/src/coalgebras/ |
H A D | lbtreeScript.sml | 61 ``is_lbtree f1 /\ is_lbtree f2 ==> 62 ((lbtree_abs f1 = lbtree_abs f2) = (f1 = f2))``,
|
H A D | pathScript.sml | 1072 ``!f1 g1 f2 g2. (pgenerate f1 g1 = pgenerate f2 g2) = 1073 (f1 = f2) /\ (g1 = g2)``,
|
H A D | llistScript.sml | 474 ``!f1 f2 x1 x2. (LUNFOLD f1 x1 = LUNFOLD f2 x2) = 477 (f1 y1 = NONE) /\ (f2 y2 = NONE) \/ 479 (f1 y1 = SOME (t1, h)) /\ (f2 y2 = SOME (t2, h)) /\ R t1 t2``, 482 Q.EXISTS_TAC `\x1 x2. LUNFOLD f1 x1 = LUNFOLD f2 x2` THEN
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | Holmake.sml | 44 f1 forces_update_of f2 46 f1 exists /\ (f2 exists ==> f1 is newer than f2)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | lisp_equalScript.sml | 651 \\ Q.ABBREV_TAC `f2 = (a - 16w =+ r5) f1` 652 \\ Q.ABBREV_TAC `f3 = (a - 12w =+ r6) f2` 711 \\ Q.UNABBREV_TAC `f1` \\ Q.UNABBREV_TAC `f2` \\ Q.UNABBREV_TAC `f3`
|
H A D | lisp_proofScript.sml | 847 ``!xs ys f1 f2. 849 DRESTRICT f2 (COMPL (LIST_TO_SET xs))) ==> 850 (VarBind f1 xs ys = VarBind f2 xs ys)``,
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_stepScript.sml | 3163 (!f f2 b s. f2 <> f ==> 3164 (ARM_READ_STATUS f (ARM_WRITE_STATUS f2 b s) = ARM_READ_STATUS f s)) /\ 3174 (!f f2 b s. ARM_READ_STATUS f (ARM_WRITE_STATUS_SPSR f2 b s) = 3221 \\ TRY (Cases_on `f2`) 3242 (!f f2 b s. ARM_READ_STATUS_SPSR f (ARM_WRITE_STATUS f2 b s) = 3249 (!f f2 b s. f <> f2 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_stepScript.sml | 3164 (!f f2 b s. f2 <> f ==> 3165 (ARM_READ_STATUS f (ARM_WRITE_STATUS f2 b s) = ARM_READ_STATUS f s)) /\ 3175 (!f f2 b s. ARM_READ_STATUS f (ARM_WRITE_STATUS_SPSR f2 b s) = 3222 \\ TRY (Cases_on `f2`) 3243 (!f f2 b s. ARM_READ_STATUS_SPSR f (ARM_WRITE_STATUS f2 b s) = 3250 (!f f2 b s. f <> f2 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/lambda/basics/ |
H A D | generic_termsScript.sml | 1154 `LIST_REL RR TS (MAP f1 TS) ==> LIST_REL RR TS (MAP f2 TS)` >> 1155 qsuff_tac `MAP f1 TS = MAP f2 TS` >- srw_tac [][] >> 1157 map_every qunabbrev_tac [`f1`, `f2`, `TS`] >>
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/ |
H A D | io_onestepScript.sml | 1314 `!f1 f2 f3 imm1 imm2 abs1 abs2 osmpl1 osmpl2 ismpl1 ismpl2 strm1 strm2 strm3. 1315 CORRECT f1 f2 imm1 abs1 osmpl1 ismpl1 strm1 strm2 /\ 1316 CORRECT f2 f3 imm2 abs2 osmpl2 ismpl2 strm2 strm3 ==>
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | mechReasoning.sml | 565 val (ir2,(pre_p2,post_p2),stk_f,(ins2,f2,outs2)) = get_spec_info (concl ir2_spec); 574 val sc_f = combinSyntax.mk_o (f2,f1); 1160 val (ir2,(pre_p2,post_p2),stk_f,(ins2,f2,outs2)) = get_spec_info (hd specL2); 1173 [mk_comb(cj_cond,initV), mk_comb(f1,initV), mk_comb(f2,initV)]));
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_OPTIMISER.sml | 468 | mergePattern(ArgPattTuple{filter=n1, allConst=c1, fromFields=f1}, ArgPattTuple{filter=n2, allConst=c2, fromFields=f2}) = 473 then ArgPattTuple{filter=n1, allConst=c1 andalso c2, fromFields = f1 andalso f2} 474 else if f1 andalso f2 482 ArgPattTuple{filter=union, allConst=c1 andalso c2, fromFields = f1 andalso f2}
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/step/ |
H A D | x64_stepLib.sml | 802 val process_float_flags2 = process_float_flags `[f1 : bool # flags; f2]` 803 val process_float_flags4 = process_float_flags `[f1 : bool # flags; f2; f3; f4]`
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | prop_logicScript.sml | 56 [`P`,`\(f1,f2). P f1 /\ P f2`]
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
H A D | DerivedBddRules.sml | 146 fun fn3(f1,f2,f3)(x1,x2,x3) = (f1 x1, f2 x2, f3 x3)
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/ml/ |
H A D | typeSoundScript.sml | 54 ``FLOOKUP (f1 f_o_f f2) k = 55 case FLOOKUP f2 k of 844 BIJ f2 tvs2 tvs3 ��� 845 raconv f2 tvs2 tvs3 t2 t3 ��� 846 raconv (f2 o f1) tvs1 tvs3 t1 t3``,
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/ |
H A D | x64Script.sml | 2692 Let(TP[Var("f2",PTy(bTy,fTy)),Var("r2",F64)], 2710 Var("f2",PTy(bTy,fTy))]),qVar"state"))))))))) 2735 Let(TP[Var("f2",PTy(bTy,fTy)),Var("r2",F32)], 2774 Var("f2",PTy(bTy,fTy)), 2946 Let(TP[Var("f2",PTy(bTy,fTy)),Var("r2",F64)], 2961 Var("f2",PTy(bTy,fTy))]),qVar"state"))))))))) 2984 Let(TP[Var("f2",PTy(bTy,fTy)),Var("r2",F32)], 3015 Var("f2",PTy(bTy,fTy)), 3237 Let(TP[Var("f2",fTy),Var("d2",F32)], 3264 TP[LF,Var("f2",fT [all...] |
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | rich_listScript.sml | 359 `!f1 f2 l. FILTER f1 (FILTER f2 l) = FILTER f2 (FILTER f1 l)`, 376 `!f1 f2 l. FILTER f1 (MAP f2 l) = MAP f2 (FILTER (f1 o f2) l)`,
|