equal
deleted
inserted
replaced
85 (* This is not limited to the first assumption *) |
85 (* This is not limited to the first assumption *) |
86 lemma |
86 lemma |
87 assumes "PROP P \<equiv> PROP Q" |
87 assumes "PROP P \<equiv> PROP Q" |
88 shows "PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q" |
88 shows "PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q" |
89 by (rewrite at asm assms) |
89 by (rewrite at asm assms) |
|
90 |
|
91 (* Rewriting "at asm" selects each full assumption, not any parts *) |
|
92 lemma |
|
93 assumes "(PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP S \<Longrightarrow> PROP R)" |
|
94 shows "PROP S \<Longrightarrow> (PROP P \<Longrightarrow> PROP Q) \<Longrightarrow> PROP R" |
|
95 apply (rewrite at asm assms) |
|
96 apply assumption |
|
97 done |
90 |
98 |
91 |
99 |
92 |
100 |
93 (* Rewriting with conditional rewriting rules works just as well. *) |
101 (* Rewriting with conditional rewriting rules works just as well. *) |
94 lemma test_theorem: |
102 lemma test_theorem: |