| changeset 26555 | 046e63c9165c |
| parent 26513 | 6f306c8c2c54 |
| child 26739 | 947b6013e863 |
--- a/src/HOL/ex/NormalForm.thy Thu Apr 03 23:55:11 2008 +0200 +++ b/src/HOL/ex/NormalForm.thy Fri Apr 04 13:40:21 2008 +0200 @@ -8,8 +8,6 @@ imports Main "~~/src/HOL/Real/Rational" begin -declare equals_eq [symmetric, code post] - lemma "True" by normalization lemma "p \<longrightarrow> True" by normalization declare disj_assoc [code func]