--- a/src/HOL/Quot/HQUOT.thy Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(* Title: HOL/Quot/HQUOT.thy
- ID: $Id$
- Author: Oscar Slotosch
- Copyright 1997 Technische Universitaet Muenchen
-
-quotient constructor for higher order quotients
-
-*)
-
-HQUOT = PER +
-
-typedef 'a quot = "{s::'a::per set. ? r.!y. y:s=y===r}" (quotNE)
-
-(* constants for equivalence classes *)
-consts
- peclass :: "'a::per => 'a quot"
- any_in :: "'a::per quot => 'a"
-
-syntax "@ecl" :: "'a::per => 'a quot" ("<[ _ ]>")
-
-translations "<[x]>" == "peclass x"
-
-defs
- peclass_def "<[x]> == Abs_quot {y. y===x}"
- any_in_def "any_in f == @x.<[x]>=f"
-end
-