src/HOL/Typedef.thy
 changeset 23710 a8ac2305eaf2 parent 23433 c2c10abd2a1e child 24269 4b2aac7669b3
```     1.1 --- a/src/HOL/Typedef.thy	Tue Jul 10 17:30:50 2007 +0200
1.2 +++ b/src/HOL/Typedef.thy	Tue Jul 10 17:30:51 2007 +0200
1.3 @@ -29,10 +29,10 @@
1.4    "(Rep x = Rep y) = (x = y)"
1.5  proof
1.6    assume "Rep x = Rep y"
1.7 -  hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
1.8 -  also have "Abs (Rep x) = x" by (rule Rep_inverse)
1.9 -  also have "Abs (Rep y) = y" by (rule Rep_inverse)
1.10 -  finally show "x = y" .
1.11 +  then have "Abs (Rep x) = Abs (Rep y)" by (simp only:)
1.12 +  moreover have "Abs (Rep x) = x" by (rule Rep_inverse)
1.13 +  moreover have "Abs (Rep y) = y" by (rule Rep_inverse)
1.14 +  ultimately show "x = y" by simp
1.15  next
1.16    assume "x = y"
1.17    thus "Rep x = Rep y" by (simp only:)
1.18 @@ -43,10 +43,10 @@
1.19    shows "(Abs x = Abs y) = (x = y)"
1.20  proof
1.21    assume "Abs x = Abs y"
1.22 -  hence "Rep (Abs x) = Rep (Abs y)" by (simp only:)
1.23 -  also from x have "Rep (Abs x) = x" by (rule Abs_inverse)
1.24 -  also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
1.25 -  finally show "x = y" .
1.26 +  then have "Rep (Abs x) = Rep (Abs y)" by (simp only:)
1.27 +  moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse)
1.28 +  moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse)
1.29 +  ultimately show "x = y" by simp
1.30  next
1.31    assume "x = y"
1.32    thus "Abs x = Abs y" by (simp only:)
1.33 @@ -76,8 +76,8 @@
1.34    shows "P y"
1.35  proof -
1.36    have "P (Rep (Abs y))" by (rule hyp)
1.37 -  also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
1.38 -  finally show "P y" .
1.39 +  moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse)
1.40 +  ultimately show "P y" by simp
1.41  qed
1.42
1.43  lemma Abs_induct [induct type]:
1.44 @@ -85,9 +85,9 @@
1.45    shows "P x"
1.46  proof -
1.47    have "Rep x \<in> A" by (rule Rep)
1.48 -  hence "P (Abs (Rep x))" by (rule r)
1.49 -  also have "Abs (Rep x) = x" by (rule Rep_inverse)
1.50 -  finally show "P x" .
1.51 +  then have "P (Abs (Rep x))" by (rule r)
1.52 +  moreover have "Abs (Rep x) = x" by (rule Rep_inverse)
1.53 +  ultimately show "P x" by simp
1.54  qed
1.55
1.56  lemma Rep_range:
```