src/HOL/Quot/PER.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quot/PER.thy	Fri Apr 04 16:01:14 1997 +0200
@@ -0,0 +1,20 @@
+(*  Title:      HOL/Quot/PER.thy
+    ID:         $Id$
+    Author:     Oscar Slotosch
+    Copyright   1997 Technische Universitaet Muenchen
+
+instances for per - makes PER higher order
+*)
+
+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) |}
+
+end