/seL4-l4v-10.1.1/isabelle/lib/Tools/ |
H A D | latex | 90 RC="$?" 95 RC="$?" 100 RC="$?" 105 RC="$?" 109 RC="$?" 116 exit "$RC"
|
H A D | browser | 93 RC="$?" 107 RC=0 110 exit "$RC"
|
/seL4-l4v-10.1.1/l4v/isabelle/lib/Tools/ |
H A D | latex | 90 RC="$?" 95 RC="$?" 100 RC="$?" 105 RC="$?" 109 RC="$?" 116 exit "$RC"
|
H A D | browser | 93 RC="$?" 107 RC=0 110 exit "$RC"
|
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/lambda/ |
H A D | etaScript.sml | 66 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 D | reductionScript.sml | 199 ���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 D | betaScript.sml | 1552 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 D | relationScript.sml | 100 ``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 D | semanticsScript.sml | 1787 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 D | reductionScript.sml | 253 ���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 D | x64.sml | 18 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 D | x64.sig | 18 OM: bool, PE: bool, PM: bool, RC: BitsN.nbit, Reserved: BitsN.nbit,
|
H A D | x64Script.sml | 15 ("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 D | chap3Script.sml | 840 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 D | summacs.tex | 46 \def\RC{{\tt\char'175}}
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | rulesScript.sml | 37 | RC of DATA 45 (mread st (RC c) = c)`;
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | CFL_RulesScript.sml | 39 | RC of DATA 46 (mread st (RC c) = c)`;
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | rulesScript.sml | 38 | RC of DATA 46 (mread st (RC c) = c)`;
|
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | listScript.sml | 3147 ``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 D | generalHelpersScript.sml | 152 ``!Rel f. WF Rel /\ (!y. (RC Rel) (f y) y)
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | theories.tex | 4345 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 D | pred_setScript.sml | 5333 Take the RC of the P argument to consider only pairs of distinct elements.
|