--- 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
--- 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