# HG changeset patch
# User slotosch
# Date 861975199 -7200
# Node ID 3d7a6130113776816abd9d0770f4ae4a55066e99
# Parent  9d6526cacc3c94888f720db72742a7ebc73c8b49
used explcite tactics in instances (since ax_per_trans "loops")

diff -r 9d6526cacc3c -r 3d7a61301137 src/HOL/Quot/FRACT.thy
--- a/src/HOL/Quot/FRACT.thy	Fri Apr 25 15:31:51 1997 +0200
+++ b/src/HOL/Quot/FRACT.thy	Fri Apr 25 15:33:19 1997 +0200
@@ -9,7 +9,7 @@
 FRACT = NPAIR + HQUOT +
 instance 
 	NP::per	
-	{| (etac per_sym_NP 1) THEN (etac per_trans_NP 1) THEN (atac 1) |}
+	{| (etac per_trans_NP 1) THEN (atac 1) THEN (etac per_sym_NP 1) |}
 
 (* now define fractions *)
 
@@ -20,4 +20,4 @@
 	half ::	"fract"
 
 defs    half_def    "half == <[abs_NP(1,2)]>"
-end
\ No newline at end of file
+end
diff -r 9d6526cacc3c -r 3d7a61301137 src/HOL/Quot/PER.thy
--- a/src/HOL/Quot/PER.thy	Fri Apr 25 15:31:51 1997 +0200
+++ b/src/HOL/Quot/PER.thy	Fri Apr 25 15:33:19 1997 +0200
@@ -8,13 +8,7 @@
 
 PER = PER0 +  (* instance for per *)
 
-(* does not work 
-instance fun  :: (per,per)per (per_sym_fun,per_trans_fun)
-
-needss explicite proofs:
-*)
-
 instance fun  :: (per,per)per   
-{| (etac per_sym_fun 1) THEN (etac per_trans_fun 1) THEN (atac 1) |}
+{| (etac per_trans_fun 1) THEN (atac 1) THEN (etac per_sym_fun 1) |}
 
 end