| changeset 19756 | 61c4117345c6 |
| parent 19683 | 3620e494cef2 |
| child 21210 | c17fd2df4e9e |
| 19755:90f80de04c46 | 19756:61c4117345c6 |
|---|---|
115 |
115 |
116 eq_reflection: "(x=y) ==> (x==y)" |
116 eq_reflection: "(x=y) ==> (x==y)" |
117 iff_reflection: "(P<->Q) ==> (P==Q)" |
117 iff_reflection: "(P<->Q) ==> (P==Q)" |
118 |
118 |
119 |
119 |
120 lemmas strip = impI allI |
|
121 |
|
122 |
|
120 text{*Thanks to Stephan Merz*} |
123 text{*Thanks to Stephan Merz*} |
121 theorem subst: |
124 theorem subst: |
122 assumes eq: "a = b" and p: "P(a)" |
125 assumes eq: "a = b" and p: "P(a)" |
123 shows "P(b)" |
126 shows "P(b)" |
124 proof - |
127 proof - |