Isabelle2016-1: remove references to empty 'assms'

Isabelle now only creates a local fact named 'assms' when there is a
non-zero number of structured assumptions.

proof/crefine/Retype_C.thy

@@ -7004,7 +7004,6 @@ lemma createObject_untypedRange:
 
 lemma createObject_capRange:
 shows "\<lbrace>P\<rbrace>createObject ty ptr us dev \<lbrace>\<lambda>m s. capRange m = {ptr.. ptr + 2 ^ (APIType_capBits ty us) - 1}\<rbrace>"
-  using assms
   apply (simp add:createObject_def)
   apply (case_tac "ty")
     apply (simp_all add:toAPIType_def ARM_H.toAPIType_def)

proof/drefine/KHeap_DR.thy

@@ -1868,7 +1868,6 @@ lemma set_list_modify_corres_helper:
   proof (induct update_list)
     case Nil
     show ?case
-      using assms
       apply (clarsimp simp:tcb_filter_modify_def)
       apply (clarsimp simp: return_def simpler_modify_def mapM_x_def sequence_x_def corres_underlying_def)
      done
@@ -3277,7 +3276,6 @@ shows "\<lbrakk>length cref \<le> n ; length cref \<le> 32; cap = transform_cap
 proof (induct n arbitrary: cref cap' cap)
   case 0
   show ?case
-    using assms
     apply clarify
     apply (case_tac "\<not> is_cnode_cap cap'")
      apply (subst cdl_resolve_address_bits_error_branch1,simp)

proof/invariant-abstract/Retype_AI.thy

@@ -702,7 +702,6 @@ lemma unat_of_nat_shift:
      apply (rule less_le_trans[OF range_cover_n_less(2)])
      apply clarsimp
     apply (erule diff_le_mono2)
-  using assms
   apply (simp add:range_cover_def)+
  done
 

proof/refine/CSpace1_R.thy

@@ -6910,7 +6910,7 @@ lemmas p_next_eq_src = mdb_ptr_src.p_next_eq
 
 lemma next_m_n:
   shows "m \<turnstile> p \<leadsto> p' = n \<turnstile> s_d_swp p \<leadsto> s_d_swp p'"
-  using assms src dest
+  using src dest
   apply (simp add: n_def n'_def modify_map_mdb_cap const_def)
   apply (simp add: s_d_swap_def)
   apply (rule conjI, clarsimp)

proof/refine/Detype_R.thy

@@ -3940,7 +3940,7 @@ proof -
                           atLeastatMost_subset_iff atLeastLessThan_iff
                           Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
   assume "gz = (objBitsKO val) + us"
-  thus ?thesis using assms
+  thus ?thesis
     apply -
     apply (rule hoare_gen_asm)
     apply (clarsimp simp:createObjects'_def split_def new_cap_addrs_fold')

proof/refine/Refine.thy

@@ -486,8 +486,7 @@ lemma kernelEntry_invs':
 
 lemma absKState_correct':
   "\<lbrakk>einvs s; invs' s'; (s,s') \<in> state_relation\<rbrakk>
-   \<Longrightarrow> absKState s' = abs_state s" 
-  using assms
+   \<Longrightarrow> absKState s' = abs_state s"
   apply (intro state.equality, simp_all add: absKState_def abs_state_def)
            apply (rule absHeap_correct)
                apply (clarsimp simp: valid_state_def valid_pspace_def)+

proof/refine/TcbAcc_R.thy

@@ -2543,7 +2543,7 @@ apply (simp add: tcb_in_cur_domain'_def)
 apply (rule hoare_assume_pre)
 apply simp
 apply (rule_tac f="ksCurDomain" in hoare_lift_Pf)
-apply (wp threadSet_obj_at'_strongish getObject_tcb_wp | simp add: assms)+
+apply (wp threadSet_obj_at'_strongish getObject_tcb_wp | simp)+
 done
 
 lemma threadSet_sch_act_wf: