/seL4-l4v-10.1.1/seL4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/ |
H A D | types.h | 30 seL4_Word tls_base, fs, gs; member in struct:seL4_UserContext_
|
/seL4-l4v-10.1.1/HOL4/examples/computability/ |
H A D | recursivefnsScript.sml | 20 recCn (f:num list -> num option) gs l = 21 let results = MAP (��g : num list -> num option. g l) gs 41 (���f gs m. recfn f (LENGTH gs) ��� EVERY (��g. recfn g m) gs ��� 42 recfn (recCn f gs) m) ��� 55 `SOME o Cn f gs = recCn (SOME o f) (MAP (��g. SOME o g) gs)` 137 Induct_on ���recfn��� >> rw[] >> rename [���gs ��� []���] >> 138 Cases_on ���gs��� >> f [all...] |
H A D | primrecfnsScript.sml | 54 Cn (f:num list -> num) (gs:(num list -> num) list) (l:num list) = 55 f (MAP (��g. g l) gs) 87 (���f gs m. primrec f (LENGTH gs) ��� EVERY (��g. primrec g m) gs ��� 88 primrec (Cn f gs) m) ��� 161 Induct_on `gs` THEN SRW_TAC [][], 186 Induct_on `gs` THEN SRW_TAC [][], 728 ``EVERY (��g. primrec g k ��� ���J. ���l. (LENGTH l = k) ==> g l < H J (SUM l)) gs 730 ���J. ���l. (LENGTH l = k) ==> SUM (MAP (��g. g l) gs) < [all...] |
/seL4-l4v-10.1.1/HOL4/src/meson/src/ |
H A D | jrhTactics.sml | 32 | rotate_p1 ((g::gs), just) = 33 let val newgs = gs @ [g] 38 | rotate_n1 (gs, just) = 39 let val (newg, newgs) = (last gs, butlast gs) 75 let val (gs, jf) = T (map ASSUME asl, g) value 76 val newgs = map (fn (asl, g) => (map concl asl, g)) gs
|
H A D | mesonLib.sml | 517 (fn (gs,(newinsts,newoffset,newsize)) => 520 val g' = Subgoal(g,gs,apprule,offset,locin) 522 if (globin = insts) andalso null(gs) then 533 | g::gs => 555 exp_goals depth (gs,stup) 556 (cacheconts (fn (gs',ftup) => cont(g'::gs',ftup))))) 722 fun meson_to_hol insts cpos_cache cvdb (Subgoal(g,gs,(n,th),offset,locin)) = 727 val ths = map (meson_to_hol newins cpos_cache cvdb) gs
|
/seL4-l4v-10.1.1/HOL4/src/num/termination/ |
H A D | selftest.sml | 37 val gs_def = DefineSchema`(gs 0 y = x + y) /\ (gs x y = x)`;
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/32/ |
H A D | machine_asm.S | 24 movw %ax, %gs 54 movw %ax, %gs
|
H A D | traps.S | 25 pushl %gs; \ 426 popl %gs 515 pushl %gs # save GS
|
/seL4-l4v-10.1.1/HOL4/examples/computability/lambda/ |
H A D | prtermScript.sml | 1506 LAM "f" (LAM "gs" (LAM "x" ( 1507 VAR "gs" 1533 ``���i f gs x. 1534 MEM i gs ��� (Phi i x = NONE) ��� 1535 (bnf_of (crecCn @@ f @@ cvlist (MAP church gs) @@ church x) = NONE)``, 1538 ���i f gs x. MEM i gs ��� (Phi i x = NONE) ��� 1539 (bnf_of (LL gs @@ NN f @@ CC x @@ cnil) = NONE) 1542 ���i f gs k x. MEM i gs ��� (Ph [all...] |
/seL4-l4v-10.1.1/seL4/src/arch/x86/64/ |
H A D | machine_asm.S | 89 movw %ax, %gs
|
H A D | traps.S | 60 /* If using multicore our gs base is set to point to a nodeInfo_t structure. 66 #define LOAD_USER_CONTEXT movq %gs:16, %rsp 68 #define LOAD_KERNEL_STACK movq %gs:0, %rsp 69 #define LOAD_IRQ_STACK(x) movq %gs:8, %x
|
/seL4-l4v-10.1.1/HOL4/src/proofman/ |
H A D | goalStack.sml | 174 val gs = return(GSTK{prop=prop,final=final, value 176 in expand_msg dpth gs ; gs end 192 fun expand tac gs = expandf (Tactical.VALID tac) gs; 193 fun expand_list ltac gs = expand_listf (Tactical.VALID_LT ltac) gs;
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | helperLib.sml | 533 fun AUTO_EXISTS_TAC (gs,goal) = EXISTS_TAC (fst (dest_exists goal)) (gs,goal) 1128 fun aux (hs,gs) = let 1129 val (v,n) = dest_exists gs 1138 THEN SIMP_TAC (std_ss++star_ss) []) (hs,gs) end 1143 fun prepare_tac (hs,gs) = let 1144 val (x,y) = pred_setSyntax.dest_in gs 1151 val thi = auto_prove "SEP_READ_TAC" (mk_imp(mk_conj(tm,gs),gs),REPEAT STRIP_TAC) 1152 in MATCH_MP_TAC thi (hs,gs) en [all...] |
/seL4-l4v-10.1.1/HOL4/examples/zipper/ |
H A D | zipperScript.sml | 245 ``zpure (o) <*> fs <*> gs <*> xs = fs <*> (gs <*> xs)``,
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibSolver.sml | 69 | contr th gs = map (C CONTR th) gs; 73 fn gs => S.CONS (SOME (contr th gs), K S.NIL));
|
H A D | mlibMeson.sml | 452 | mp env th (g :: gs) (th1 :: p) = 453 mp env (RESOLVE (formula_subst env g) (INST env th1) th) gs p 456 fun modus_ponens th gs (state as {env, ...}) = 457 update_proof (mp env (INST env th) (rev gs)) state;
|
H A D | metisTools.sml | 400 fun order_cl (cl,gs,_,_,_) [] = (cl,gs)
|
/seL4-l4v-10.1.1/HOL4/src/patricia/ |
H A D | sptreeSyntax.sml | 201 fun sys gs d = syspr {gravs = gs, depth = d, binderp = false}
|
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/concurrent/ |
H A D | Task_Queue.sml | 215 fun group_tasks (Queue {groups, ...}) gs = 218 gs Tasks.empty
|
/seL4-l4v-10.1.1/HOL4/examples/logic/ |
H A D | foltypesScript.sml | 334 ``GFVl [] = {} ��� GFVl (g::gs) = GFV g ��� GFVl gs``,
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
H A D | compilerLib.sml | 274 val gs = (map strip_forall o list_dest dest_conj o fst o dest_imp o concl) imp value 275 val xs = zip (rev fnames) gs
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | exportLib.sml | 70 val gs = tm |> rator |> rand |> dest_graph value 73 in (xs,ys,gs,ep) end
|
H A D | derive_specsLib.sml | 119 in mk_TRACE_SPLIT (map (fn (th,gs,nexts) => 120 TRACE_STEP (p, gs, th, mk_TRACE_SPLIT (map 121 (fn n => aux (n:int) (p::seen) (gs:term)) nexts))) ys) end)
|
/seL4-l4v-10.1.1/HOL4/src/holyhammer/legacy/ |
H A D | hh_tac.ml | 171 let fOL_TAC2 ((ps,gl) as gs) = 174 rULE_ASSUM_TAC (cONV_RULE (fOL_CONV mindata))) gs;;
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | type_grammar.sml | 365 fun merge_acc acc (gs as (g1, g2)) = 366 case gs of
|