# HG changeset patch
# User wenzelm
# Date 1490286047 -3600
# Node ID 2ffda850f844df9bda7c8e8e7c53d5daf38630bc
# Parent  27144776aefe3b2df9894e306a30ba417acc59d3
tuned proof;

diff -r 27144776aefe -r 2ffda850f844 src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Mon Mar 20 21:53:37 2017 +0100
+++ b/src/CTT/CTT.thy	Thu Mar 23 17:20:47 2017 +0100
@@ -285,11 +285,7 @@
 
 text \<open>Compare with standard version: \<open>B\<close> is applied to UNSIMPLIFIED expression!\<close>
 lemma SumIL2: "\<lbrakk>c = a : A; d = b : B(a)\<rbrakk> \<Longrightarrow> <c,d> = <a,b> : Sum(A,B)"
-  apply (rule sym_elem)
-  apply (rule SumIL)
-   apply (rule_tac [!] sym_elem)
-   apply assumption+
-  done
+  by (rule sym_elem) (rule SumIL; rule sym_elem)
 
 lemmas intrL2_rls = NI_succL ProdIL SumIL2 PlusI_inlL PlusI_inrL