equal
deleted
inserted
replaced
53 apply (blast del: rtranclp.rtrancl_refl intro: rtranclp.rtrancl_into_rtrancl)+ |
53 apply (blast del: rtranclp.rtrancl_refl intro: rtranclp.rtrancl_into_rtrancl)+ |
54 -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *} |
54 -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *} |
55 done |
55 done |
56 |
56 |
57 |
57 |
58 subsection {* Misc properties of par-beta *} |
58 subsection {* Misc properties of @{text "par_beta"} *} |
59 |
59 |
60 lemma par_beta_lift [simp]: |
60 lemma par_beta_lift [simp]: |
61 "t => t' \<Longrightarrow> lift t n => lift t' n" |
61 "t => t' \<Longrightarrow> lift t n => lift t' n" |
62 by (induct t arbitrary: t' n) fastsimp+ |
62 by (induct t arbitrary: t' n) fastsimp+ |
63 |
63 |