author | urbanc |
Fri, 20 Apr 2007 00:28:07 +0200 | |
changeset 22732 | 5bd1a2a94e1b |
parent 22731 | abfdccaed085 |
child 22733 | 0b14bb35be90 |
--- 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