isabelle: src/HOL/Quot/NPAIR.ML@3aced7fa7d8b (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
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	9	goalw thy [rep_NP_def] "rep_NP(abs_NP np) = np";
3457 a8ab7c64817c Ran expandshort paulson parents: 2906 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
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	15	val prems = goalw thy [per_NP_def] "eqv (x::NP) y ==> eqv y x";
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	16	by (cut_facts_tac prems 1);
3457 a8ab7c64817c Ran expandshort paulson parents: 2906 diff changeset	17	by (Auto_tac());
2906 171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	18	qed "per_sym_NP";
171dedbc9bdb Example for higher order quotients: Fractionals slotosch parents: diff changeset	19

author	paulson
	Tue, 01 Jul 1997 17:34:42 +0200
changeset 3477	3aced7fa7d8b
parent 3457	a8ab7c64817c
child 4477	b3e5857d8d99
permissions	-rw-r--r--