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
     1 (*  Title:      HOL/Quot/NPAIR.ML
     2     ID:         $Id$
     3     Author:     Oscar Slotosch
     4     Copyright   1997 Technische Universitaet Muenchen
     5 
     6 *)
     7 open NPAIR;
     8 
     9 Goalw [rep_NP_def] "rep_NP(abs_NP np) = np";
    10 by Auto_tac;
    11 qed "rep_abs_NP";
    12 
    13 Addsimps [rep_abs_NP];
    14 
    15 Goalw [per_NP_def] "eqv (x::NP) y ==> eqv y x";
    16 by Auto_tac;
    17 qed "per_sym_NP";
    18