author | paulson |
Thu, 11 Nov 1999 10:25:17 +0100 | |
changeset 8005 | b64d86018785 |
parent 5858 | beddc19c107a |
permissions | -rw-r--r-- |
(* Title: HOL/Quot/NPAIR.ML ID: $Id$ Author: Oscar Slotosch Copyright 1997 Technische Universitaet Muenchen *) open NPAIR; Goalw [rep_NP_def] "rep_NP(abs_NP np) = np"; by Auto_tac; qed "rep_abs_NP"; Addsimps [rep_abs_NP]; Goalw [per_NP_def] "eqv (x::NP) y ==> eqv y x"; by Auto_tac; qed "per_sym_NP";