src/HOL/Quot/FRACT.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 3059 3d7a61301137
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/Quot/FRACT.thy
     2     ID:         $Id$
     3     Author:     Oscar Slotosch
     4     Copyright   1997 Technische Universitaet Muenchen
     5 
     6 Example for higher order quotients: fractions
     7 *)
     8 
     9 FRACT = NPAIR + HQUOT +
    10 instance 
    11 	NP::per	
    12 	{| (etac per_trans_NP 1) THEN (atac 1) THEN (etac per_sym_NP 1) |}
    13 
    14 (* now define fractions *)
    15 
    16 types fract = NP quot
    17 
    18 (* example for fractions *)
    19 consts 
    20 	half ::	"fract"
    21 
    22 defs    half_def    "half == <[abs_NP(1,2)]>"
    23 end