Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Quot/PER.thy
author slotosch
Fri, 25 Apr 1997 15:31:51 +0200
changeset 3058 9d6526cacc3c
parent 2904 fc10751254aa
child 3059 3d7a61301137
permissions -rw-r--r--
changed Domain->Dom for SML/NJ

(*  Title:      HOL/Quot/PER.thy
    ID:         $Id$
    Author:     Oscar Slotosch
    Copyright   1997 Technische Universitaet Muenchen

instances for per - makes PER higher order
*)

PER = PER0 +  (* instance for per *)

(* does not work 
instance fun  :: (per,per)per (per_sym_fun,per_trans_fun)

needss explicite proofs:
*)

instance fun  :: (per,per)per   
{| (etac per_sym_fun 1) THEN (etac per_trans_fun 1) THEN (atac 1) |}

end
isabelle