src/HOL/Quot/PER.thy

--- a/src/HOL/Quot/PER.thy	Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(*  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 *)
-
-instance fun  :: (per,per)per   
-{| (etac per_trans_fun 1) THEN (atac 1) THEN (etac per_sym_fun 1) |}
-
-end