(* typed combinators, version in RTA'05 paper *) theory tca imports Gen tcadef WfUn rewr begin instance tc :: tr apply intro_classes ; apply (erule_tac tca_runul_tys) ; apply (erule_tac tca_redstd_tys) ; apply (erule_tac tca_redstd_mono) ; apply (rule_tac tca_rd1) ; apply (erule_tac tc_wty_unique) ; apply assumption ; done ; end