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

2906 171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	1	(* Title: HOL/Quot/NPAIR.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 NPAIR;
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	8
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4477 diff changeset	9	Goalw [rep_NP_def] "rep_NP(abs_NP np) = np";
4477 b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort paulson parents: 3457 diff changeset	10	by Auto_tac;
2906 171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	11	qed "rep_abs_NP";
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	12
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	13	Addsimps [rep_abs_NP];
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	14
5858 beddc19c107a needed tidying desperately paulson parents: 5069 diff changeset	15	Goalw [per_NP_def] "eqv (x::NP) y ==> eqv y x";
4477 b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort paulson parents: 3457 diff changeset	16	by Auto_tac;
2906 171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	17	qed "per_sym_NP";
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	18

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