src/HOL/Library/Permutations.thy
changeset 32456 341c83339aeb
parent 30663 0b6aff7451b2
child 32960 69916a850301
child 32988 d1d4d7a08a66
     1.1 --- a/src/HOL/Library/Permutations.thy	Sat Aug 29 14:31:39 2009 +0200
     1.2 +++ b/src/HOL/Library/Permutations.thy	Mon Aug 31 14:09:42 2009 +0200
     1.3 @@ -843,9 +843,7 @@
     1.4  	unfolding permutes_def by metis+
     1.5        from eq have "(Fun.swap a b id o p) a  = (Fun.swap a c id o q) a" by simp
     1.6        hence bc: "b = c"
     1.7 -	apply (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong)
     1.8 -	apply (cases "a = b", auto)
     1.9 -	by (cases "b = c", auto)
    1.10 +	by (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong split: split_if_asm)
    1.11        from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o p) = (\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o q)" by simp
    1.12        hence "p = q" unfolding o_assoc swap_id_idempotent
    1.13  	by (simp add: o_def)