isabelle: src/HOL/Quot/FRACT.thy@406eb27fe53c (annotated)

2906 171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	1	(* Title: HOL/Quot/FRACT.thy
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
2910 905aa895136c * empty log message * slotosch parents: 2906 diff changeset	6	Example for higher order quotients: fractions
2906 171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	7	*)
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	8
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	9	FRACT = NPAIR + HQUOT +
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	10	instance
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	11	NP::per
3059 3d7a61301137 used explcite tactics in instances (since ax_per_trans "loops") slotosch parents: 2910 diff changeset	12	{\| (etac per_trans_NP 1) THEN (atac 1) THEN (etac per_sym_NP 1) \|}
2906 171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	13
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	14	(* now define fractions *)
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	15
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	16	types fract = NP quot
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	17
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	18	(* example for fractions *)
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	19	consts
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	20	half :: "fract"
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	21
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	22	defs half_def "half == <[abs_NP(1,2)]>"
3059 3d7a61301137 used explcite tactics in instances (since ax_per_trans "loops") slotosch parents: 2910 diff changeset	23	end

author	wenzelm
	Thu, 19 Nov 1998 11:47:22 +0100
changeset 5936	406eb27fe53c
parent 3059	3d7a61301137
permissions	-rw-r--r--