# HG changeset patch # User urbanc # Date 1177021687 -7200 # Node ID 5bd1a2a94e1b535b3fa73ea535967e0f9ba2656a # Parent abfdccaed08531e0e504b6bb8481f6c89e70f18b declared lemmas true_eqvt and false_eqvt to be equivariant (suggested by samth at ccs.neu.edu) diff -r abfdccaed085 -r 5bd1a2a94e1b src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Thu Apr 19 18:23:11 2007 +0200 +++ b/src/HOL/Nominal/Nominal.thy Fri Apr 20 00:28:07 2007 +0200 @@ -3167,7 +3167,8 @@ lemmas [eqvt] = (* connectives *) - if_eqvt imp_eqvt disj_eqvt conj_eqvt neg_eqvt + if_eqvt imp_eqvt disj_eqvt conj_eqvt neg_eqvt + true_eqvt false_eqvt (* datatypes *) perm_unit.simps