isabelle: src/HOL/Quot/NPAIR.ML@beddc19c107a (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	paulson
	Fri, 13 Nov 1998 13:41:53 +0100
changeset 5858	beddc19c107a
parent 5069	3ea049f7979d
permissions	-rw-r--r--