Lines Matching defs:compatible
326 (* Define compatible relations on the object/method language. *)
329 val compatible =
330 new_definition ("compatible",
331 ���compatible Ro Rd Re Rm =
374 (compatible Ro Rd Re Rm /\
382 (compatible Ro Rd Re Rm /\
392 (* page 51. This is the compatible closure of R. *)
836 (* 1) compatible (in the sense of Barendregt, Definition 3.1.1, pg 50 *)
837 (* 2) the compatible closure of the R relation, in the sense of *)
844 ���!R. compatible
846 REWRITE_TAC[compatible]
961 (* 1) compatible (in the sense of Barendregt, Definition 3.1.1, pg 50 *)
1012 ���!R. compatible
1014 REWRITE_TAC[compatible]
1021 THEN IMP_RES_TAC (REWRITE_RULE[compatible] RED1_compatible)
1028 (REWRITE_RULE[compatible] RED_compatible));
1222 (* 1) compatible (in the sense of Barendregt, Definition 3.1.1, pg 50 *)
1226 (* 4) an equality relation, as a compatible equivalence relation. *)
1293 ���!R. compatible
1298 REWRITE_TAC[compatible]
1312 (REWRITE_RULE[compatible] REQUAL_compatible));