isabelle: src/HOL/Quot/PER.ML@58e37d59c146 (annotated)

2904 fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	1	(* Title: HOL/Quot/PER.ML
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	*)
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	7	open PER;
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	8
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 3842 diff changeset	9	Goalw [fun_per_def,per_def] "f===g=(!x y. x:D&y:D&x===y-->f x===g y)";
3457 a8ab7c64817c Ran expandshort paulson parents: 2904 diff changeset	10	by (rtac refl 1);
2904 fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	11	qed "inst_fun_per";
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	12
fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	13	(* Witness that quot is not empty *)
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 3842 diff changeset	14	Goal "?z:{s.? r.!y. y:s=y===r}";
6162 484adda70b65 expandshort paulson parents: 5858 diff changeset	15	by (rtac CollectI 1);
2904 fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	16	by (res_inst_tac [("x","x")] exI 1);
3457 a8ab7c64817c Ran expandshort paulson parents: 2904 diff changeset	17	by (rtac allI 1);
a8ab7c64817c Ran expandshort paulson parents: 2904 diff changeset	18	by (rtac mem_Collect_eq 1);
2904 fc10751254aa (partial) equivalecne relations. classes er<per slotosch parents: diff changeset	19	qed "quotNE";

author	wenzelm
	Thu, 16 Mar 2000 00:32:55 +0100
changeset 8488	58e37d59c146
parent 6162	484adda70b65
permissions	-rw-r--r--