src/HOL/Algebra/Bij.thy
changeset 67091 1393c2340eec
parent 63167 0909deb8059b
child 67443 3abf6a722518
     1.1 --- a/src/HOL/Algebra/Bij.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Algebra/Bij.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -67,7 +67,7 @@
     1.4   shows "\<lbrakk>h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S\<rbrakk>
     1.5          \<Longrightarrow> inv_into S h (g x y) = g (inv_into S h x) (inv_into S h y)"
     1.6  apply (simp add: Bij_def bij_betw_def)
     1.7 -apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' & y = h y'", clarify)
     1.8 +apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' \<and> y = h y'", clarify)
     1.9   apply (simp add: eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem], blast)
    1.10  done
    1.11