Lines Matching defs:TC
50 (* This defines TC in the logic as TC R is the transitive closure of R, *)
53 (* induction tactics, cases theorems, etc. It's theory "TC". *)
64 val (TC,Ru'v') = strip_comb ant
69 (*val (TC,[R,u',v']) = strip_comb ant*)
70 (*val {Name = "TC",...} = dest_const TC*)
71 val _ = if #Name(dest_const TC) = "TC" then true else raise Match
91 ���!R (a:'a) b. TC R a b ==>
93 (?d. R b d /\ TC R c d)))���,
114 ���!R (a:'a) b. TC R a b ==>
115 (DIAMOND R ==> (!c. TC R a c ==>
116 (?d. TC R b d /\ TC R c d)))���,
136 ���!R:'a->'a->bool. DIAMOND R ==> DIAMOND (TC R)���,
1593 TC R = R-arrow with "*" superscript after = transitive closure
1718 ���!R t1:^term t2. TC (RC (RED1 R)) t1 t2
1730 ���!t1:^term t2. TC (RC (RED1 BETA_R)) t1 t2
1743 ==> TC (RC (RED1 R)) t1 t2���,
1754 ���!R:^term_rel. TC (RC (RED1 R)) = RED R���,
1769 ���!t1:^term t2. TC REDL t1 t2 ==> RED BETA_R t1 t2���,
1779 TC R1 a b ==> (!x y. R1 x y ==> R2 x y) ==> TC R2 a b���),
1796 (TC R1 a b ==> TC R2 a b)���,
1806 ���TC (REDL:^term_rel) = RED BETA_R���,