| changeset 40872 | 7c556a9240de |
| parent 40703 | d1fc454d6735 |
| child 41076 | a7fba340058c |
--- a/src/HOL/Set.thy Wed Dec 01 21:03:02 2010 +0100 +++ b/src/HOL/Set.thy Thu Dec 02 14:34:58 2010 +0100 @@ -882,7 +882,6 @@ lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P" by blast - subsubsection {* Some rules with @{text "if"} *} text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}