isabelle: src/HOL/Quot/PER.thy@0b268cff9344 (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
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	9	PER = PER0 + (* instance for per *)
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	wenzelm
	Tue, 27 May 1997 15:45:07 +0200
changeset 3362	0b268cff9344
parent 3059	3d7a61301137
child 4531	20a7fddb706a
permissions	-rw-r--r--