isabelle: src/HOL/Quot/PER.thy@ecdedff41e67 (annotated)

2904 fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	1	(* Title: HOL/Quot/PER.thy
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	2	ID: $Id$
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	3	Author: Oscar Slotosch
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	4	Copyright 1997 Technische Universitaet Muenchen
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	5
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	6	instances for per - makes PER higher order
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	7	*)
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	8
4531 20a7fddb706a streamlined specification of included theories oheimb parents: 3059 diff changeset	9	PER = PER0 + (* instance for per *)
2904 fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	10
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	11	instance fun :: (per,per)per
3059 3d7a61301137 used explcite tactics in instances (since ax_per_trans "loops") slotosch parents: 2904 diff changeset	12	{\| (etac per_trans_fun 1) THEN (atac 1) THEN (etac per_sym_fun 1) \|}
2904 fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	13
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	14	end

author	paulson
	Tue, 30 Nov 1999 17:53:34 +0100
changeset 8042	ecdedff41e67
parent 4531	20a7fddb706a
permissions	-rw-r--r--