Searched refs:OBJ (Results 1 - 8 of 8) sorted by relevance

/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/
H A Dmakefile7 OBJ = bddio.o bddop.o bvec.o cache.o fdd.o imatrix.o kernel.o \ macro
32 libbdd.a: $(OBJ) ../config
33 ar r libbdd.a $(OBJ)
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/
H A DsemanticsScript.sml285 THEN MP_TAC (SPECL [���l:^dict���,���OBJ l���,���lb:string���]
293 ���!d l x L. ((invoke (OBJ d) l) <[ [x,L]) =
294 invoke ((OBJ d) <[ [x,L]) l���,
375 ���!d lb mth x L. ((update (OBJ d) lb mth) <[ [x,L]) =
376 update ((OBJ d) <[ [x,L]) lb (mth <[ [x,L])���,
392 (* INVOKE (OBJ d) l or UPDATE (OBJ d) l m *)
404 (^SIGMA_R (INVOKE (OBJ d) l) (invoke (OBJ d) l)) /\
408 (^SIGMA_R (UPDATE (OBJ
[all...]
H A DreductionScript.sml336 (!d1 d2. Rd d1 d2 ==> Ro (OBJ d1) (OBJ d2) /\
420 (^RED1_obj R (OBJ d1) (OBJ d2))) /\
483 (!R d1 d2. P_1 R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\
604 (!R d1 d2. P_1 R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\
641 P_1 R d1 d2 /\ RED1_dict R d1 d2 ==> P_0 R (OBJ d1) (OBJ d
[all...]
H A DliftScript.sml1305 {def_name="OBJ_def", fname="OBJ",
1661 (!d. dict_Prop d ==> obj_Prop (OBJ d)) /\
1736 (!d. dict_Prop d ==> obj_Prop (OBJ d)) /\
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/
H A Dcompile212 *.c | *.cpp | *.CPP | *.lib | *.LIB | *.Lib | *.OBJ | *.obj | *.[oO])
/seL4-l4v-10.1.1/HOL4/src/Boolify/test/
H A Ddatatypes.sml262 | OBJ of (string # method) list
285 /\ (FV_obj (OBJ d) = FV_dict d)
/seL4-l4v-10.1.1/HOL4/src/unwind/
H A DunwindLib.sml325 (* REW = {ti | p ti} and OBJ = {ti | ~p ti} *)
/seL4-l4v-10.1.1/HOL4/src/quotient/Manual/
H A Dquotient.tex5293 {def_name="OBJ_def", fname="OBJ",
5466 \> ($\forall$v. P0 (OVAR v)) $\wedge$ ($\forall$l. P2 l $\Rightarrow$ P0 (OBJ l)) $\wedge$ \\
5559 \>\> ($\forall$d. hom\_o (OBJ d) = obj (hom\_d d) d) $\wedge$ \\
5576 % (!d. hom_o (OBJ d) = obj (hom_d d)) /\

Completed in 130 milliseconds