equal
deleted
inserted
replaced
148 assume "P(x)" |
148 assume "P(x)" |
149 then show R |
149 then show R |
150 proof (rule r) |
150 proof (rule r) |
151 { fix y y' |
151 { fix y y' |
152 assume "P(y)" and "P(y')" |
152 assume "P(y)" and "P(y')" |
153 with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac 1")+ |
153 with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac @{context} 1")+ |
154 then have "y = y'" by (rule subst) |
154 then have "y = y'" by (rule subst) |
155 } note r' = this |
155 } note r' = this |
156 show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'" by (intro strip, elim conjE) (rule r') |
156 show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'" by (intro strip, elim conjE) (rule r') |
157 qed |
157 qed |
158 qed |
158 qed |