| changeset 12327 | 5a4d78204492 |
| parent 11456 | 7eb63f63e6c6 |
| child 15243 | ba52fdc2c4e8 |
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Thu Nov 29 01:51:38 2001 +0100 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Thu Nov 29 13:33:45 2001 +0100 @@ -162,7 +162,7 @@ normality of @{term"normif"}: *} -lemma[simp]: "\<forall>t e. normal(normif b t e) = (normal t \<and> normal e)"; +lemma [simp]: "\<forall>t e. normal(normif b t e) = (normal t \<and> normal e)"; (*<*) apply(induct_tac b); by(auto);