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
slotosch@2904
     1
(*  Title:      HOL/Quot/PER.thy
slotosch@2904
     2
    ID:         $Id$
slotosch@2904
     3
    Author:     Oscar Slotosch
slotosch@2904
     4
    Copyright   1997 Technische Universitaet Muenchen
slotosch@2904
     5
slotosch@2904
     6
instances for per - makes PER higher order
slotosch@2904
     7
*)
slotosch@2904
     8
oheimb@4531
     9
PER = PER0 + (* instance for per *)
slotosch@2904
    10
slotosch@2904
    11
instance fun  :: (per,per)per   
slotosch@3059
    12
{| (etac per_trans_fun 1) THEN (atac 1) THEN (etac per_sym_fun 1) |}
slotosch@2904
    13
slotosch@2904
    14
end