equal
deleted
inserted
replaced
230 next |
230 next |
231 assume "x = y" |
231 assume "x = y" |
232 thus "x == y" by (rule eq_reflection) |
232 thus "x == y" by (rule eq_reflection) |
233 qed |
233 qed |
234 |
234 |
235 lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" |
235 lemma atomize_conj [atomize]: |
|
236 "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" |
236 proof |
237 proof |
237 assume "!!C. (A ==> B ==> PROP C) ==> PROP C" |
238 assume "!!C. (A ==> B ==> PROP C) ==> PROP C" |
238 show "A & B" by (rule conjI) |
239 show "A & B" by (rule conjI) |
239 next |
240 next |
240 fix C |
241 fix C |