changeset 47988 | e4b69e10b990 |
parent 46950 | d0181abdbdac |
child 48891 | c0eafbd55de3 |
--- a/src/HOL/Hilbert_Choice.thy Thu May 24 17:05:30 2012 +0200 +++ b/src/HOL/Hilbert_Choice.thy Thu May 24 17:25:53 2012 +0200 @@ -443,7 +443,7 @@ have "h ` A = B" proof safe fix a assume "a \<in> A" - thus "h a \<in> B" using SUB1 2 3 by (case_tac "a \<in> A'", auto) + thus "h a \<in> B" using SUB1 2 3 by (cases "a \<in> A'") auto next fix b assume *: "b \<in> B" show "b \<in> h ` A"