src/HOL/Quot/NPAIR.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 5858 beddc19c107a
permissions -rw-r--r--
tidied; added lemma restrict_to_left
slotosch@2906
     1
(*  Title:      HOL/Quot/NPAIR.ML
slotosch@2906
     2
    ID:         $Id$
slotosch@2906
     3
    Author:     Oscar Slotosch
slotosch@2906
     4
    Copyright   1997 Technische Universitaet Muenchen
slotosch@2906
     5
slotosch@2906
     6
*)
slotosch@2906
     7
open NPAIR;
slotosch@2906
     8
wenzelm@5069
     9
Goalw [rep_NP_def] "rep_NP(abs_NP np) = np";
paulson@4477
    10
by Auto_tac;
slotosch@2906
    11
qed "rep_abs_NP";
slotosch@2906
    12
slotosch@2906
    13
Addsimps [rep_abs_NP];
slotosch@2906
    14
paulson@5858
    15
Goalw [per_NP_def] "eqv (x::NP) y ==> eqv y x";
paulson@4477
    16
by Auto_tac;
slotosch@2906
    17
qed "per_sym_NP";
slotosch@2906
    18