isabelle: src/HOL/Quot/FRACT.ML@484adda70b65 (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
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4089 diff changeset	8	Goalw [per_def,per_NP_def]
3842 b55686a7b22c fixed dots; wenzelm parents: 2906 diff changeset	9	"(op ===)=(%x y. fst(rep_NP x)snd(rep_NP y)=fst(rep_NP y)snd(rep_NP x))";
6162 484adda70b65 expandshort paulson parents: 5858 diff changeset	10	by (rtac refl 1);
2906 171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	11	qed "inst_NP_per";
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	12
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	13
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4089 diff changeset	14	Goalw [half_def] "half = <[abs_NP(n,2*n)]>";
6162 484adda70b65 expandshort paulson parents: 5858 diff changeset	15	by (rtac per_class_eqI 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3842 diff changeset	16	by (simp_tac (simpset() addsimps [inst_NP_per]) 1);
2906 171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	17	qed "test";

author	paulson
	Fri, 29 Jan 1999 16:26:12 +0100
changeset 6162	484adda70b65
parent 5858	beddc19c107a
child 8791	50b650d19641
permissions	-rw-r--r--