diff -r 8b0b414e71b0 -r 3b8e3a156200 thys/PDerivs.thy
--- a/thys/PDerivs.thy	Wed Feb 20 00:00:30 2019 +0000
+++ b/thys/PDerivs.thy	Sat Feb 23 21:52:06 2019 +0000
@@ -358,27 +358,30 @@
        apply(simp)
       apply(simp)
      apply(simp add: pders_CHAR)
+(*  SEQ case *)
     apply(simp)
     apply(rule subset_trans)
      apply(rule pders_SEQ)
     defer
+(* ALT case *)
     apply(simp)
     apply(rule impI)
     apply(rule conjI)
   apply blast
-  apply blast
+    apply blast
+(* STAR case *)
     apply(case_tac s)
     apply(simp)
    apply(rule subset_trans)
   thm pders_STAR
      apply(rule pders_STAR)
      apply(simp)
-    apply(simp)
-  apply (smt UN_I UN_least Un_iff insertCI pders_Set_def subsetCE subsetI)
+    apply(auto simp add: pders_Set_def)[1]
   apply(simp)
   apply(rule conjI)
-  apply blast
-  by (metis Un_insert_right le_supI1 pders_Set_subsetI subset_trans sup_ge2)
+   apply blast
+apply(auto simp add: pders_Set_def)[1]
+  done
 
 fun size2 :: "rexp \<Rightarrow> nat" where
   "size2 ZERO = 1" |
@@ -403,15 +406,18 @@
        apply(simp)
       apply(simp)
      apply(simp)
+(* SEQ case *)
     apply(simp)
     apply(auto)[1]
   apply (smt Suc_n_not_le_n add.commute distrib_left le_Suc_eq left_add_mult_distrib nat_le_linear trans_le_add1)
   apply (smt Suc_le_mono Suc_n_not_le_n le_trans nat_le_linear power2_eq_square power2_sum semiring_normalization_rules(23) trans_le_add2)
   apply (smt Groups.add_ac(3) Suc_n_not_le_n distrib_left le_Suc_eq left_add_mult_distrib nat_le_linear trans_le_add1)
+(*  ALT case  *)
    apply(simp)
    apply(auto)[1]
   apply (smt Groups.add_ac(2) Suc_le_mono Suc_n_not_le_n le_add2 linear order_trans power2_eq_square power2_sum)
   apply (smt Groups.add_ac(2) Suc_le_mono Suc_n_not_le_n left_add_mult_distrib linear mult.commute order.trans trans_le_add1)
+(* STAR case *)
   apply(auto)[1]
   apply(drule_tac x="r'" in bspec)
    apply(simp)