# HG changeset patch
# User haftmann
# Date 1184081451 -7200
# Node ID a8ac2305eaf23db68bfe5f607741086404ebe91c
# Parent  fd31da8f752a9ec44e1a49986aad1bd6b8f1c8e6
removed proof dependency on transitivity theorems

diff -r fd31da8f752a -r a8ac2305eaf2 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Tue Jul 10 17:30:50 2007 +0200
+++ b/src/HOL/Typedef.thy	Tue Jul 10 17:30:51 2007 +0200
@@ -29,10 +29,10 @@
   "(Rep x = Rep y) = (x = y)"
 proof
   assume "Rep x = Rep y"
-  hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
-  also have "Abs (Rep x) = x" by (rule Rep_inverse)
-  also have "Abs (Rep y) = y" by (rule Rep_inverse)
-  finally show "x = y" .
+  then have "Abs (Rep x) = Abs (Rep y)" by (simp only:)
+  moreover have "Abs (Rep x) = x" by (rule Rep_inverse)
+  moreover have "Abs (Rep y) = y" by (rule Rep_inverse)
+  ultimately show "x = y" by simp
 next
   assume "x = y"
   thus "Rep x = Rep y" by (simp only:)
@@ -43,10 +43,10 @@
   shows "(Abs x = Abs y) = (x = y)"
 proof
   assume "Abs x = Abs y"
-  hence "Rep (Abs x) = Rep (Abs y)" by (simp only:)
-  also from x have "Rep (Abs x) = x" by (rule Abs_inverse)
-  also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
-  finally show "x = y" .
+  then have "Rep (Abs x) = Rep (Abs y)" by (simp only:)
+  moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse)
+  moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse)
+  ultimately show "x = y" by simp
 next
   assume "x = y"
   thus "Abs x = Abs y" by (simp only:)
@@ -76,8 +76,8 @@
   shows "P y"
 proof -
   have "P (Rep (Abs y))" by (rule hyp)
-  also from y have "Rep (Abs y) = y" by (rule Abs_inverse)
-  finally show "P y" .
+  moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse)
+  ultimately show "P y" by simp
 qed
 
 lemma Abs_induct [induct type]:
@@ -85,9 +85,9 @@
   shows "P x"
 proof -
   have "Rep x \<in> A" by (rule Rep)
-  hence "P (Abs (Rep x))" by (rule r)
-  also have "Abs (Rep x) = x" by (rule Rep_inverse)
-  finally show "P x" .
+  then have "P (Abs (Rep x))" by (rule r)
+  moreover have "Abs (Rep x) = x" by (rule Rep_inverse)
+  ultimately show "P x" by simp
 qed
 
 lemma Rep_range: