Searched refs:RC (Results 1 - 22 of 22) sorted by relevance

/seL4-l4v-10.1.1/isabelle/lib/Tools/
H A Dlatex90 RC="$?"
95 RC="$?"
100 RC="$?"
105 RC="$?"
109 RC="$?"
116 exit "$RC"
H A Dbrowser93 RC="$?"
107 RC=0
110 exit "$RC"
/seL4-l4v-10.1.1/l4v/isabelle/lib/Tools/
H A Dlatex90 RC="$?"
95 RC="$?"
100 RC="$?"
105 RC="$?"
109 RC="$?"
116 exit "$RC"
H A Dbrowser93 RC="$?"
107 RC=0
110 exit "$RC"
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/lambda/
H A DetaScript.sml66 val (RC,Ru'v') = strip_comb ant value
71 (*val (RC,[R,u',v']) = strip_comb ant*)
72 (*val {Name = "RC",...} = dest_const RC*)
73 val _ = if #Name(dest_const RC) = "RC" then true else raise Match
688 RC R2 a b ==>
691 ?d. TC (RC R2) b d /\ RC R1 c d) ==>
693 ?d. RC R
[all...]
H A DreductionScript.sml199 ���RC (R:'a->'a->bool) a b =
208 ���!R (x:'a). RC R x x���,
216 ���!R (x:'a) y. R x y ==> RC R x y���,
228 ==> !u v. RC R u v ==> P u v���,
243 (*val (RC,[R,u',v']) = strip_comb ant*)
244 val (RC,Ruv) = strip_comb ant value
246 val _ = assert (curry op = "RC") (#Name (dest_const RC))
262 ���!R (x:'a) y. RC R x y ==> R x y \/ (x = y)���,
320 ���!R:^term_rel. compatible R ==> compatible (RC
[all...]
H A DbetaScript.sml1552 val (RC,Ru'v') = strip_comb ant value
1557 (*val (RC,[R,u',v']) = strip_comb ant*)
1558 (*val {Name = "RC",...} = dest_const RC*)
1559 val _ = if #Name(dest_const RC) = "RC" then true else raise Match
1581 RC (RED1 BETA_R) SUBSET REDL SUBSET RED BETA_R
1592 RC R = R-arrow with "=" underneath = reflexive closure
1599 ���!t1:^term t2. RC BETA_R t1 t2 ==> REDL t1 t2���,
1636 ���!t1:^term t2. RC (RED
[all...]
/seL4-l4v-10.1.1/HOL4/src/relation/
H A DrelationScript.sml100 ``RC (R:'a->'a->bool) x y = (x = y) \/ R x y``);
108 ``EQC (R:'a->'a->bool) = RC (TC (SC R))``);
189 ``!R:'a->'a->bool. reflexive (RC R)``,
196 ``(!x y. R x y ==> R (f x) (f y)) ==> !x y. RC R x y ==> RC R (f x) (f y)``,
201 ``(!x y. R x y ==> Q x y) ==> RC R x y ==> RC Q x y``,
207 ``(!x y. P x /\ R x y ==> P y) ==> (!x y. P x /\ RC R x y ==> P y)``,
212 ``(!x y. R x y ==> (f x = f y)) ==> (!x y. RC R x y ==> (f x = f y))``,
233 ``!R. symmetric (RC
[all...]
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/
H A DsemanticsScript.sml1787 val (RC,Ru'v') = boolSyntax.strip_comb ant value
1792 (*val (RC,[R,u',v']) = boolSyntax.strip_comb ant*)
1793 (*val {Name = "RC",...} = dest_const RC*)
1794 val _ = if #Name(dest_const RC) = "RC" then true else raise Match
1816 RC (RED1 SIGMA_R) SUBSET REDL SUBSET RED SIGMA_R
1827 RC R = R-arrow with "=" underneath = reflexive closure
1885 ���(!o1 o2. RC (RED1_obj SIGMA_R) o1 o2 ==> REDL_obj o1 o2) /\
1886 (!d1 d2. RC (RED1_dic
[all...]
H A DreductionScript.sml253 ���RC (R:'a->'a->bool) a b =
262 ���!R (x:'a). RC R x x���,
270 ���!R (x:'a) y. R x y ==> RC R x y���,
282 ==> !u v. RC R u v ==> P u v���,
297 val (RC,[R,u',v']) = boolSyntax.strip_comb ant value
298 val {Name = "RC",...} = dest_const RC
314 ���!R (x:'a) y. RC R x y ==> R x y \/ (x = y)���,
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/
H A Dx64.sml18 OM: bool, PE: bool, PM: bool, RC: BitsN.nbit, Reserved: BitsN.nbit,
598 fun MXCSR_DAZ_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC,
601 OM = OM, PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = UE,
604 fun MXCSR_DE_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved,
607 OM = OM, PE = PE, PM = PM, RC = RC, Reserved = Reserved, UE = UE,
610 fun MXCSR_DM_rupd ({DAZ, DE, DM, FZ, IE, IM, OE, OM, PE, PM, RC, Reserved,
613 OM = OM, PE = PE, PM = PM, RC = RC, Reserve
[all...]
H A Dx64.sig18 OM: bool, PE: bool, PM: bool, RC: BitsN.nbit, Reserved: BitsN.nbit,
H A Dx64Script.sml15 ("OE",bTy),("OM",bTy),("PE",bTy),("PM",bTy),("RC",FTy 2),
237 bVar"OE",bVar"OM",bVar"PE",bVar"PM",Var("RC",FTy 2),
239 CC[Var("Reserved",F16),Mop(Cast F1,bVar"FZ"),Var("RC",FTy 2),
2306 CS(Dest("RC",FTy 2,Dest("MXCSR",CTy"MXCSR",qVar"state")),
/seL4-l4v-10.1.1/HOL4/examples/lambda/barendregt/
H A Dchap3Script.sml840 Q_TAC SUFF_TAC `!M N. RC (compat_closure beta) M N ==> grandbeta M N`
974 (* |- !R. diamond_property R ==> diamond_property (RC R) *)
1207 Q_TAC SUFF_TAC `diamond_property (RC (compat_closure eta))` THEN1
1218 (!x y z. R1 x y /\ R2 x z ==> ?w. RTC R1 z w /\ RC R2 y w) ==>
1226 `?w. RC R2 y w /\ RTC R1 z' w` by PROVE_TAC [] THEN
1267 ?Q. reduction eta P Q /\ RC (-b->) N Q`
/seL4-l4v-10.1.1/HOL4/src/res_quan/Manual/
H A Dsummacs.tex46 \def\RC{{\tt\char'175}}
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A DrulesScript.sml37 | RC of DATA
45 (mread st (RC c) = c)`;
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A DCFL_RulesScript.sml39 | RC of DATA
46 (mread st (RC c) = c)`;
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A DrulesScript.sml38 | RC of DATA
46 (mread st (RC c) = c)`;
/seL4-l4v-10.1.1/HOL4/src/list/src/
H A DlistScript.sml3147 ``total (RC R) ==> total (RC (SHORTLEX R))``,
3287 ``total (RC R) ==> total (RC (LLEX R))``,
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/
H A DgeneralHelpersScript.sml152 ``!Rel f. WF Rel /\ (!y. (RC Rel) (f y) y)
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/
H A Dtheories.tex4345 Le chiusure riflessiva~(\holtxt{RC}) e simmetrica~(\holtxt{SC}) sono
4352 RC_DEF |- RC R x y = (x = y) \/ R x y
4354 EQC_DEF |- EQC R = RC (TC (SC R))
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/
H A Dpred_setScript.sml5333 Take the RC of the P argument to consider only pairs of distinct elements.

Completed in 311 milliseconds