1.1 --- a/src/HOL/Quot/FRACT.thy	Fri Apr 25 15:31:51 1997 +0200
     1.2 +++ b/src/HOL/Quot/FRACT.thy	Fri Apr 25 15:33:19 1997 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  FRACT = NPAIR + HQUOT +
     1.5  instance 
     1.6  	NP::per	
     1.7 -	{| (etac per_sym_NP 1) THEN (etac per_trans_NP 1) THEN (atac 1) |}
     1.8 +	{| (etac per_trans_NP 1) THEN (atac 1) THEN (etac per_sym_NP 1) |}
     1.9  
    1.10  (* now define fractions *)
    1.11  
    1.12 @@ -20,4 +20,4 @@
    1.13  	half ::	"fract"
    1.14  
    1.15  defs    half_def    "half == <[abs_NP(1,2)]>"
    1.16 -end
    1.17 \ No newline at end of file
    1.18 +end

     2.1 --- a/src/HOL/Quot/PER.thy	Fri Apr 25 15:31:51 1997 +0200
     2.2 +++ b/src/HOL/Quot/PER.thy	Fri Apr 25 15:33:19 1997 +0200
     2.3 @@ -8,13 +8,7 @@
     2.4  
     2.5  PER = PER0 +  (* instance for per *)
     2.6  
     2.7 -(* does not work 
     2.8 -instance fun  :: (per,per)per (per_sym_fun,per_trans_fun)
     2.9 -
    2.10 -needss explicite proofs:
    2.11 -*)
    2.12 -
    2.13  instance fun  :: (per,per)per   
    2.14 -{| (etac per_sym_fun 1) THEN (etac per_trans_fun 1) THEN (atac 1) |}
    2.15 +{| (etac per_trans_fun 1) THEN (atac 1) THEN (etac per_sym_fun 1) |}
    2.16  
    2.17  end