Lines Matching defs:TC
43 (* This defines TC in the logic as TC R is the transitive closure of R, *)
46 (* induction tactics, cases theorems, etc. It's theory "TC". *)
57 val (TC,Ru'v') = strip_comb ant
62 (*val (TC,[R,u',v']) = strip_comb ant*)
63 (*val {Name = "TC",...} = dest_const TC*)
64 val _ = if #Name(dest_const TC) = "TC" then true else raise Match
335 ���!(R:^term_rel) t1 t2. TC R t1 t2 ==>
337 (!u. TC R (App u t1) (App u t2)) /\
338 (!u. TC R (App t1 u) (App t2 u)) /\
339 (!x. TC R (Lam x t1) (Lam x t2))���),
364 ���!(R:^term_rel). compatible R ==> compatible (TC R)���,
660 ���!R:^term_rel. compatible (TC (RC (RED1 R)))���,