isabelle: src/HOL/Quot/FRACT.ML@0b268cff9344 (annotated)

2906 171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	1	(* Title: HOL/Quot/FRACT.ML
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	2	ID: $Id$
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	3	Author: Oscar Slotosch
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	4	Copyright 1997 Technische Universitaet Muenchen
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	5
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	6	*)
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	7	open FRACT;
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	8
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	9	goalw thy [per_def,per_NP_def]
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	10	"(op ===)=(%x y.fst(rep_NP x)snd(rep_NP y)=fst(rep_NP y)snd(rep_NP x))";
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	11	fr refl;
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	12	qed "inst_NP_per";
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	13
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	14
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	15	goalw thy [half_def] "half = <[abs_NP(n,2*n)]>";
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	16	fr per_class_eqI;
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	17	by (simp_tac (!simpset addsimps [inst_NP_per]) 1);
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	18	qed "test";

author	wenzelm
	Tue, 27 May 1997 15:45:07 +0200
changeset 3362	0b268cff9344
parent 2906	171dedbc9bdb
child 3842	b55686a7b22c
permissions	-rw-r--r--