src/HOL/UNITY/Transformers.thy
changeset 21733 131dd2a27137
parent 21312 1d39091a3208
child 23767 7272a839ccd9
     1.1 --- a/src/HOL/UNITY/Transformers.thy	Sat Dec 09 18:06:17 2006 +0100
     1.2 +++ b/src/HOL/UNITY/Transformers.thy	Sun Dec 10 07:12:26 2006 +0100
     1.3 @@ -444,11 +444,11 @@
     1.4  apply (rule subsetI)  
     1.5  apply (erule wens_set.induct)
     1.6    txt{*Basis*} 
     1.7 -  apply (force simp add: wens_single_finite_def)
     1.8 +  apply (fastsimp simp add: wens_single_finite_def)
     1.9   txt{*Wens inductive step*}
    1.10 - apply (case_tac "acta = Id", simp)   
    1.11 + apply (case_tac "acta = Id", simp)
    1.12   apply (simp add: wens_single_eq)
    1.13 - apply (elim disjE)   
    1.14 + apply (elim disjE)
    1.15   apply (simp add: wens_single_Un_eq)
    1.16   apply (force simp add: wens_single_finite_Un_eq)
    1.17  txt{*Union inductive step*}