src/HOL/Predicate.thy
changeset 23389 aaca6a8e5414
parent 22846 fb79144af9a3
child 23708 b5eb0b4dd17d
     1.1 --- a/src/HOL/Predicate.thy	Thu Jun 14 18:33:29 2007 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Thu Jun 14 18:33:31 2007 +0200
     1.3 @@ -34,11 +34,11 @@
     1.4  proof
     1.5    fix S
     1.6    assume "!!S. PROP P S"
     1.7 -  show "PROP P (Collect S)" .
     1.8 +  then show "PROP P (Collect S)" .
     1.9  next
    1.10    fix S
    1.11    assume "!!S. PROP P (Collect S)"
    1.12 -  have "PROP P {x. x : S}" .
    1.13 +  then have "PROP P {x. x : S}" .
    1.14    thus "PROP P S" by simp
    1.15  qed
    1.16  
    1.17 @@ -46,11 +46,11 @@
    1.18  proof
    1.19    fix S
    1.20    assume "!!S. PROP P S"
    1.21 -  show "PROP P (member S)" .
    1.22 +  then show "PROP P (member S)" .
    1.23  next
    1.24    fix S
    1.25    assume "!!S. PROP P (member S)"
    1.26 -  have "PROP P (member {x. S x})" .
    1.27 +  then have "PROP P (member {x. S x})" .
    1.28    thus "PROP P S" by simp
    1.29  qed
    1.30  
    1.31 @@ -96,11 +96,11 @@
    1.32  proof
    1.33    fix S
    1.34    assume "!!S. PROP P S"
    1.35 -  show "PROP P (Collect2 S)" .
    1.36 +  then show "PROP P (Collect2 S)" .
    1.37  next
    1.38    fix S
    1.39    assume "!!S. PROP P (Collect2 S)"
    1.40 -  have "PROP P (Collect2 (member2 S))" .
    1.41 +  then have "PROP P (Collect2 (member2 S))" .
    1.42    thus "PROP P S" by simp
    1.43  qed
    1.44  
    1.45 @@ -108,11 +108,11 @@
    1.46  proof
    1.47    fix S
    1.48    assume "!!S. PROP P S"
    1.49 -  show "PROP P (member2 S)" .
    1.50 +  then show "PROP P (member2 S)" .
    1.51  next
    1.52    fix S
    1.53    assume "!!S. PROP P (member2 S)"
    1.54 -  have "PROP P (member2 (Collect2 S))" .
    1.55 +  then have "PROP P (member2 (Collect2 S))" .
    1.56    thus "PROP P S" by simp
    1.57  qed
    1.58