src/HOL/Quot/FRACT.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quot/FRACT.thy	Fri Apr 04 16:03:11 1997 +0200
@@ -0,0 +1,23 @@
+(*  Title:      HOL/Quot/FRACT.thy
+    ID:         $Id$
+    Author:     Oscar Slotosch
+    Copyright   1997 Technische Universitaet Muenchen
+
+Example for higher order quotients: fractionals
+*)
+
+FRACT = NPAIR + HQUOT +
+instance 
+	NP::per	
+	{| (etac per_sym_NP 1) THEN (etac per_trans_NP 1) THEN (atac 1) |}
+
+(* now define fractions *)
+
+types fract = NP quot
+
+(* example for fractions *)
+consts 
+	half ::	"fract"
+
+defs    half_def    "half == <[abs_NP(1,2)]>"
+end
\ No newline at end of file