--- a/src/HOL/Quot/PER.ML Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Title: HOL/Quot/PER.ML
- ID: $Id$
- Author: Oscar Slotosch
- Copyright 1997 Technische Universitaet Muenchen
-
-*)
-open PER;
-
-Goalw [fun_per_def,per_def] "f===g=(!x y. x:D&y:D&x===y-->f x===g y)";
-by (rtac refl 1);
-qed "inst_fun_per";
-
-(* Witness that quot is not empty *)
-Goal "?z:{s.? r.!y. y:s=y===r}";
-by (rtac CollectI 1);
-by (res_inst_tac [("x","x")] exI 1);
-by (rtac allI 1);
-by (rtac mem_Collect_eq 1);
-qed "quotNE";