src/HOL/Isar_examples/Cantor.thy
changeset 23373 ead82c82da9e
parent 16417 9bc16273c2d4
child 31758 3edd5f813f01
     1.1 --- a/src/HOL/Isar_examples/Cantor.thy	Wed Jun 13 16:43:02 2007 +0200
     1.2 +++ b/src/HOL/Isar_examples/Cantor.thy	Wed Jun 13 18:30:11 2007 +0200
     1.3 @@ -34,15 +34,15 @@
     1.4    proof
     1.5      assume "?S : range f"
     1.6      then obtain y where "?S = f y" ..
     1.7 -    thus False
     1.8 +    then show False
     1.9      proof (rule equalityCE)
    1.10        assume "y : f y"
    1.11 -      assume "y : ?S" hence "y ~: f y" ..
    1.12 -      thus ?thesis by contradiction
    1.13 +      assume "y : ?S" then have "y ~: f y" ..
    1.14 +      with `y : f y` show ?thesis by contradiction
    1.15      next
    1.16        assume "y ~: ?S"
    1.17 -      assume "y ~: f y" hence "y : ?S" ..
    1.18 -      thus ?thesis by contradiction
    1.19 +      assume "y ~: f y" then have "y : ?S" ..
    1.20 +      with `y ~: ?S` show ?thesis by contradiction
    1.21      qed
    1.22    qed
    1.23  qed