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