src/HOL/Quot/PER.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 4531 20a7fddb706a
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/Quot/PER.thy
     2     ID:         $Id$
     3     Author:     Oscar Slotosch
     4     Copyright   1997 Technische Universitaet Muenchen
     5 
     6 instances for per - makes PER higher order
     7 *)
     8 
     9 PER = PER0 + (* instance for per *)
    10 
    11 instance fun  :: (per,per)per   
    12 {| (etac per_trans_fun 1) THEN (atac 1) THEN (etac per_sym_fun 1) |}
    13 
    14 end