(* Title: HOL/Quot/PER.thy ID: $Id$ Author: Oscar Slotosch Copyright 1997 Technische Universitaet Muencheninstances for per - makes PER higher order*)PER = PER0 + (* instance for per *)instance fun :: (per,per)per {| (etac per_trans_fun 1) THEN (atac 1) THEN (etac per_sym_fun 1) |}end