Searched refs:OBJ (Results 1 - 8 of 8) sorted by relevance
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | makefile | 7 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 D | semanticsScript.sml | 285 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 D | reductionScript.sml | 336 (!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 D | liftScript.sml | 1305 {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 D | compile | 212 *.c | *.cpp | *.CPP | *.lib | *.LIB | *.Lib | *.OBJ | *.obj | *.[oO])
|
/seL4-l4v-10.1.1/HOL4/src/Boolify/test/ |
H A D | datatypes.sml | 262 | OBJ of (string # method) list 285 /\ (FV_obj (OBJ d) = FV_dict d)
|
/seL4-l4v-10.1.1/HOL4/src/unwind/ |
H A D | unwindLib.sml | 325 (* REW = {ti | p ti} and OBJ = {ti | ~p ti} *)
|
/seL4-l4v-10.1.1/HOL4/src/quotient/Manual/ |
H A D | quotient.tex | 5293 {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 91 milliseconds