tuned proof;
authorwenzelm
Thu Mar 23 17:20:47 2017 +0100 (2017-03-23)
changeset 653382ffda850f844
parent 65337 27144776aefe
child 65339 c4531ddafe72
tuned proof;
src/CTT/CTT.thy
     1.1 --- a/src/CTT/CTT.thy	Mon Mar 20 21:53:37 2017 +0100
     1.2 +++ b/src/CTT/CTT.thy	Thu Mar 23 17:20:47 2017 +0100
     1.3 @@ -285,11 +285,7 @@
     1.4  
     1.5  text \<open>Compare with standard version: \<open>B\<close> is applied to UNSIMPLIFIED expression!\<close>
     1.6  lemma SumIL2: "\<lbrakk>c = a : A; d = b : B(a)\<rbrakk> \<Longrightarrow> <c,d> = <a,b> : Sum(A,B)"
     1.7 -  apply (rule sym_elem)
     1.8 -  apply (rule SumIL)
     1.9 -   apply (rule_tac [!] sym_elem)
    1.10 -   apply assumption+
    1.11 -  done
    1.12 +  by (rule sym_elem) (rule SumIL; rule sym_elem)
    1.13  
    1.14  lemmas intrL2_rls = NI_succL ProdIL SumIL2 PlusI_inlL PlusI_inrL
    1.15