equal
deleted
inserted
replaced
94 apply (erule rtrancl_induct) |
94 apply (erule rtrancl_induct) |
95 apply blast |
95 apply blast |
96 apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl) |
96 apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl) |
97 done |
97 done |
98 |
98 |
99 lemma apps_preserves_betas [rulified, simp]: |
99 lemma apps_preserves_betas [rule_format, simp]: |
100 "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss" |
100 "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss" |
101 apply (induct_tac rs rule: rev_induct) |
101 apply (induct_tac rs rule: rev_induct) |
102 apply simp |
102 apply simp |
103 apply simp |
103 apply simp |
104 apply clarify |
104 apply clarify |