--- a/src/HOL/Quot/FRACT.thy Sun Jul 30 13:06:20 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(* Title: HOL/Quot/FRACT.thy
- ID: $Id$
- Author: Oscar Slotosch
- Copyright 1997 Technische Universitaet Muenchen
-
-Example for higher order quotients: fractions
-*)
-
-FRACT = NPAIR + HQUOT +
-instance
- NP::per
- {| (etac per_trans_NP 1) THEN (atac 1) THEN (etac per_sym_NP 1) |}
-
-(* now define fractions *)
-
-types fract = NP quot
-
-(* example for fractions *)
-consts
- half :: "fract"
-
-defs half_def "half == <[abs_NP(1,2)]>"
-end