| changeset 37388 | 793618618f78 |
| parent 36846 | 0f67561ed5a6 |
| child 37664 | 2946b8f057df |
--- a/src/HOL/SetInterval.thy Tue Jun 08 16:37:19 2010 +0200 +++ b/src/HOL/SetInterval.thy Tue Jun 08 16:37:22 2010 +0200 @@ -770,7 +770,7 @@ qed lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}" -apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - Suc 0"]) +apply (rule card_bij_eq [of Suc _ _ "\<lambda>x. x - Suc 0"]) apply simp apply fastsimp apply auto