diff --git a/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Map_Impl.thy b/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Map_Impl.thy
--- a/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Map_Impl.thy
+++ b/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Map_Impl.thy
@@ -1,84 +1,84 @@
 section "Hash-Maps (Interface Instantiations)"
 theory Hash_Map_Impl
 imports Imp_Map_Spec Hash_Map
 begin
 
 lemma hm_map_impl: "imp_map is_hashmap"
   apply unfold_locales
   apply (rule is_hashmap_prec)
   done
 interpretation hm: imp_map is_hashmap by (rule hm_map_impl)
 
 lemma hm_empty_impl: "imp_map_empty is_hashmap hm_new"
   apply unfold_locales
   apply (sep_auto heap: hm_new_rule)
   done
 interpretation hm: imp_map_empty is_hashmap hm_new by (rule hm_empty_impl)
 
 lemma hm_lookup_impl: "imp_map_lookup is_hashmap hm_lookup"
   apply unfold_locales
   apply (sep_auto heap: hm_lookup_rule)
   done
 interpretation hm: imp_map_lookup is_hashmap hm_lookup by (rule hm_lookup_impl)
 
 lemma hm_update_impl: "imp_map_update is_hashmap hm_update"
   apply unfold_locales
   apply (sep_auto heap: hm_update_rule)
   done
 interpretation hm: imp_map_update is_hashmap hm_update by (rule hm_update_impl)
 
 lemma hm_delete_impl: "imp_map_delete is_hashmap hm_delete"
   apply unfold_locales
   apply (sep_auto heap: hm_delete_rule)
   done
 interpretation hm: imp_map_delete is_hashmap hm_delete by (rule hm_delete_impl)
 
 lemma hm_is_empty_impl: "imp_map_is_empty is_hashmap hm_isEmpty"
   apply unfold_locales
   apply (sep_auto heap: hm_isEmpty_rule)
   done
 interpretation hm: imp_map_is_empty is_hashmap hm_isEmpty
   by (rule hm_is_empty_impl)
 
 lemma hm_size_impl: "imp_map_size is_hashmap hm_size"
   apply unfold_locales
   apply (sep_auto heap: hm_size_rule)
   done
 interpretation hm: imp_map_size is_hashmap hm_size by (rule hm_size_impl)
 
 lemma hm_iterate_impl: 
   "imp_map_iterate is_hashmap hm_is_it hm_it_init hm_it_has_next hm_it_next"
   apply unfold_locales
   apply (rule hm_it_init_rule)
-  apply (erule hm_it_next_rule)
-  apply (rule hm_it_has_next_rule)
+  apply (sep_auto heap add: hm_it_next_rule)
+  apply (sep_auto heap add: hm_it_has_next_rule)
   apply (rule ent_frame_fwd[OF hm_it_finish])
   apply (frame_inference)
   apply solve_entails
   done
 interpretation hm: 
   imp_map_iterate is_hashmap hm_is_it hm_it_init hm_it_has_next hm_it_next
   by (rule hm_iterate_impl)
 
 (*
 definition "hm_is_it'' m ht l' it \<equiv> 
   \<exists>\<^sub>Al. hm_is_it' l ht l' it * \<up>(map_of (concat l) = m)"
 
 lemma hm_iterate'_impl: 
   "imp_map_iterate' is_hashmap hm_is_it'' hm_it_init hm_it_has_next hm_it_next"
   apply unfold_locales
   apply (rule hm_it_init_rule)
   apply (erule hm_it_next_rule)
   apply (rule hm_it_has_next_rule)
   apply (rule ent_frame_fwd[OF hm_it_finish])
   apply (frame_inference)
   apply solve_entails
   done
 
 *)
 
 export_code hm_new hm_lookup hm_update hm_delete hm_isEmpty hm_size 
   hm_it_init hm_it_has_next hm_it_next
   checking SML_imp
 
 end
diff --git a/thys/Separation_Logic_Imperative_HOL/Examples/Idioms.thy b/thys/Separation_Logic_Imperative_HOL/Examples/Idioms.thy
--- a/thys/Separation_Logic_Imperative_HOL/Examples/Idioms.thy
+++ b/thys/Separation_Logic_Imperative_HOL/Examples/Idioms.thy
@@ -1,257 +1,257 @@
 section \<open>Common Proof Methods and Idioms\<close> 
 theory Idioms 
 imports "../Sep_Main" Open_List Circ_List Hash_Set_Impl
 begin 
 text_raw\<open>\label{thy:ex:idioms}\<close>
 
   text \<open>
     This theory gives a short documentation of common proof techniques and 
     idioms for the separation logic framework. For this purpose, it presents
     some proof snippets (inspired by the other example theories), and heavily
     comments on them.
 \<close>
 
   subsection \<open>The Method \<open>sep_auto\<close>\<close>
   text \<open>The most versatile method of our framework is \<open>sep_auto\<close>,
     which integrates the verification condition generator, the entailment
     solver and some pre- and postprocessing tactics based on the simplifier 
     and classical reasoner. It can be applied to a Hoare-triple or entailment
     subgoal, and will try to solve it, and any emerging new goals. It stops
     when the goal is either solved or it gets stuck somewhere.\<close>
 
   text \<open>As a simple example for \<open>sep_auto\<close> consider the following
     program that does some operations on two circular lists:\<close>
   definition "test \<equiv> do {
     l1 \<leftarrow> cs_empty;
     l2 \<leftarrow> cs_empty;
     l1 \<leftarrow> cs_append ''a'' l1;
     l2 \<leftarrow> cs_append ''c'' l2;
     l1 \<leftarrow> cs_append ''b'' l1;
     l2 \<leftarrow> cs_append ''e'' l2;
     l2 \<leftarrow> cs_prepend ''d'' l2;
     l2 \<leftarrow> cs_rotate l2;
     return (l1,l2)
   }"
   
   text \<open>The \<open>sep_auto\<close> method does all the 
     necessary frame-inference automatically, and thus manages to prove
     the following lemma in one step:\<close>
   lemma "<emp> 
     test 
     <\<lambda>(l1,l2). cs_list [''a'',''b''] l1 
       * cs_list [''c'',''e'',''d''] l2>\<^sub>t"
     unfolding test_def
     apply (sep_auto)
     done
 
   text \<open>\<open>sep_auto\<close> accepts all the section-options of the classical
     reasoner and simplifier, e.g., \<open>simp add/del:\<close>, \<open>intro:\<close>.
     Moreover, it has some more section options, the most useful being 
     \<open>heap add/del:\<close> to add or remove Hoare-rules that are applied
     with frame-inference. A complete documentation of the accepted options can
     be found in Section~\ref{sec:auto:overview}.
 \<close>
 
   text \<open>As a typical example, consider the following proof:\<close>
   lemma complete_ht_rehash: 
     "<is_hashtable l ht> ht_rehash ht 
     <\<lambda>r. is_hashtable l ht * is_hashtable (ls_rehash l) r>"
   proof -
     have LEN: " l \<noteq> [] \<Longrightarrow> Suc 0 < 2 * length l" by (cases l) auto
     show ?thesis
       apply (rule cons_pre_rule[OF ht_imp_len])
       unfolding ht_rehash_def
       apply (sep_auto 
         heap: complete_ht_new_sz complete_ht_copy
         simp: ls_rehash_def LEN
       ) \<comment> \<open>Here we add a heap-rule, and some simp-rules\<close>
       done
   qed
 
   subsection \<open>Applying Single Rules\<close>
   text \<open>\paragraph{Hoare Triples} In this example, we show how to do
     a proof step-by-step.\<close>
 
   lemma
     "<os_list xs n> os_prepend x n <os_list (x # xs)>"
     unfolding os_prepend_def
     txt \<open>The rules to deconstruct compound statements are contained in the
       \<open>sep_decon_rules\<close> collection\<close>
     thm sep_decon_rules
     apply (rule sep_decon_rules)
     txt \<open>The rules for statement that deend on the heap are
       contained in the \<open>sep_heap_rules\<close> collection. The
       \<open>fi_rule\<close>-lemma prepares frame inference for them\<close>
     apply (rule sep_heap_rules[THEN fi_rule])
     apply frame_inference \<comment> \<open>This method does the frame-inference\<close>
     
     txt \<open>The consequence rule comes in three versions, 
       \<open>const_rule\<close>, \<open>cons_pre_rule\<close>, 
       and \<open>cons_post_rule\<close>\<close>
     apply (rule cons_post_rule) 
     apply (rule sep_decon_rules)
 
     txt \<open>A simplification unfolds \<open>os_list\<close> and extract the
       pure part of the assumption\<close>
     apply (clarsimp)
 
     txt \<open>We can use \<open>ent_ex_postI\<close> to manually introduce 
       existentials in entailsments\<close>
     apply (rule_tac x=xa in ent_ex_postI)
     apply (rule_tac x=n in ent_ex_postI)
     txt \<open>The simplifier has a setup for assertions, so it will do the rest\<close>
     apply simp
     done
 
   text \<open>Note that the proof above can be done with \<open>sep_auto\<close>,
     the "Swiss army knife" of our framework\<close>
   lemma
     "<os_list xs n> os_prepend x n <os_list (x # xs)>"
     unfolding os_prepend_def by sep_auto
 
   text \<open>\paragraph{Entailment} This example presents an actual proof
     from the circular list theory, where we have to manually apply a
     rule and give some hints to frame inference\<close>
   lemma cs_append_rule: 
     "<cs_list l p> cs_append x p <cs_list (l@[x])>"
     apply (cases p)
     apply (sep_auto simp: cs_append.simps)
 
     apply (sep_auto simp: cs_append.simps heap: lseg_append)
     txt \<open>At this point, we are left with an entailment subgoal that sep-auto
       cannot solve. A closer look reveals that we could use the rule
       \<open>lseg_append\<close>. 
       
       With the \<open>ent_frame_fwd\<close>-rule, we can manually apply a rule to
       solve an entailment, involving frame inference. In this case, we have
       the additional problem that frame-inference guesses
       a wrong instantiation, and is not able to infer the frame.
       So we have to pre-instantiate the rule, as done below.\<close>
     apply (rule_tac s1=a in ent_frame_fwd[OF lseg_append])
     apply frame_inference \<comment> \<open>Now frame-inference is able to infer the frame\<close>
 
     txt \<open>Now we are left with a trivial entailment, modulo commutativity of
       star. This can be handled by the entailment solver:\<close>
     apply solve_entails
     done
 
 
 
   subsection \<open>Functions with Explicit Recursion\<close>
   text \<open>If the termination argument of a function depends on one of
     its parameters, we can use the function package. For example, 
     the following function inserts elements from a list into a hash-set:\<close>
 
   fun ins_from_list 
     :: "('x::{heap,hashable}) list \<Rightarrow> 'x hashset \<Rightarrow> 'x hashset Heap" 
     where
     "ins_from_list [] hs = return hs" |
     "ins_from_list (x # l) hs = do { hs \<leftarrow> hs_ins x hs; ins_from_list l hs }"
 
   text \<open>Proofs over such functions are usually done by structural
     induction on the explicit parameter, in this case, on the list\<close>
   lemma ins_from_list_correct:
     "<is_hashset s hs> ins_from_list l hs <is_hashset (s\<union>set l)>\<^sub>t"
   proof (induction l arbitrary: hs s)
     case (Cons x l) 
     txt \<open>In the induction step, the induction hypothesis has to be 
       declared as a heap-rule, as \<open>sep_auto\<close> currently does not
       look for potential heap-rules among the premises of the subgoal\<close>
     show ?case by (sep_auto heap: Cons.IH)
   qed sep_auto
 
 
   subsection \<open>
     Functions with Recursion Involving the Heap
 \<close>
   text \<open>If the termination argument of a function depends on data stored on
     the heap, \<open>partial_function\<close> is a useful tool.
 
     Note that, despite the name, proving a Hoare-Triple \<open><\<dots>> \<dots> <\<dots>>\<close>
     for something defined with \<open>partial_function\<close> implies total 
     correctness.
 \<close>
 
   text \<open>In the following example, we compute the sum of a list, using an
     iterator. Note that the partial-function package does not provide a
     code generator setup by default, so we have to add a \<open>[code]\<close>
     attribute manually\<close>
   partial_function (heap) os_sum' :: "int os_list_it \<Rightarrow> int \<Rightarrow> int Heap" 
     where [code]:
     "os_sum' it s = do {
       b \<leftarrow> os_it_has_next it;
       if b then do {
         (x,it') \<leftarrow> os_it_next it;
         os_sum' it' (s+x)
       } else return s
     }"
 
   text \<open>The proof that the function is correct can be done by induction
     over the representation of the list that we still have to iterate over.
     Note that for iterators over sets, we need induction on finite sets,
     cf. also \<open>To_List_Ga.thy\<close>\<close>
 
   lemma os_sum'_rule: 
     "<os_is_it l p l' it> 
     os_sum' it s 
     <\<lambda>r. os_list l p * \<up>(r = s + sum_list l')>\<^sub>t"
   proof (induct l' arbitrary: it s)
     case Nil thus ?case
       txt \<open>To unfold the definition of a partial function, we have to use 
         \<open>subst\<close>. Note that \<open>simp\<close> would loop, unfolding the
         function arbitrarily deep\<close>
       apply (subst os_sum'.simps)
       txt \<open>\<open>sep_auto\<close> accepts all the section parameters that 
         \<open>auto\<close> does, eg. \<open>intro:\<close>\<close>
-      apply (sep_auto intro: os.quit_iteration)
+      apply (sep_auto intro: os.quit_iteration ent_true_drop)
       done
   next
     case (Cons x l')
     show ?case
       apply (subst os_sum'.simps)
       txt \<open>Additionally, \<open>sep_auto\<close> accepts some more section 
         parameters. The most common one, \<open>heap:\<close>, declares rules 
         to be used with frame inference. See Section~\ref{sec:auto:overview}
         for a complete overview.\<close>
       apply (sep_auto heap: Cons.hyps)
       done
   qed
 
 
   subsection \<open>Precision Proofs\<close>
   text \<open>
     Precision lemmas show that an assertion uniquely determines some of its
     parameters. Our example shows that two list segments from the same start 
     pointer and with the same list, also have to end at the same end pointer.
 \<close>
   
   lemma lseg_prec3: 
     "\<forall>q q'. h \<Turnstile> (lseg l p q * F1) \<and>\<^sub>A (lseg l p q' * F2) \<longrightarrow> q=q'"
     apply (intro allI)
   proof (induct l arbitrary: p F1 F2)
     case Nil thus ?case 
       apply simp \<comment> \<open>A precision solver for references and arrays is included
         in the standard simplifier setup. Building a general precision solver
         remains future work.\<close>
       by metis \<comment> \<open>Unfortunately, the simplifier cannot cope with arbitrarily  
         directed equations, so we have to use some more powerful tool\<close>
   next
     case (Cons x l)
     show ?case
       apply clarsimp
   
       apply (subgoal_tac "na=n")
   
       txt \<open>The \<open>prec_frame\<close> and \<open>prec_frame'\<close> rules are 
         useful to do precision proofs\<close>
       apply (erule prec_frame'[OF Cons.hyps])
       apply frame_inference
       apply frame_inference
   
       apply (drule prec_frame[OF sngr_prec])
       apply frame_inference
       apply frame_inference
       apply simp
       done
   qed
 end
diff --git a/thys/Separation_Logic_Imperative_HOL/Examples/Imp_List_Spec.thy b/thys/Separation_Logic_Imperative_HOL/Examples/Imp_List_Spec.thy
--- a/thys/Separation_Logic_Imperative_HOL/Examples/Imp_List_Spec.thy
+++ b/thys/Separation_Logic_Imperative_HOL/Examples/Imp_List_Spec.thy
@@ -1,85 +1,85 @@
 section \<open>Interface for Lists\<close>
 theory Imp_List_Spec
 imports "../Sep_Main"
 begin
 text \<open>
   This file specifies an abstract interface for list data structures. It can
   be implemented by concrete list data structures, as demonstrated in the open
   and circular singly linked list examples.
 \<close>
 
 locale imp_list =
   fixes is_list :: "'a list \<Rightarrow> 'l \<Rightarrow> assn"
   assumes precise: "precise is_list"
     (*"\<forall>l l'. h\<Turnstile>(is_list l p * F1) \<and>\<^sub>A (is_list l' p * F2) \<longrightarrow> l=l'"*)
 
 locale imp_list_empty = imp_list +
   constrains is_list :: "'a list \<Rightarrow> 'l \<Rightarrow> assn"
   fixes empty :: "'l Heap"
   assumes empty_rule[sep_heap_rules]: "<emp> empty <is_list []>\<^sub>t"
 
 locale imp_list_is_empty = imp_list +
   constrains is_list :: "'a list \<Rightarrow> 'l \<Rightarrow> assn"
   fixes is_empty :: "'l \<Rightarrow> bool Heap"
   assumes is_empty_rule[sep_heap_rules]: 
     "<is_list l p> is_empty p <\<lambda>r. is_list l p * \<up>(r \<longleftrightarrow> l=[])>\<^sub>t"
 
 locale imp_list_append = imp_list +
   constrains is_list :: "'a list \<Rightarrow> 'l \<Rightarrow> assn"
   fixes append :: "'a \<Rightarrow> 'l \<Rightarrow> 'l Heap"
   assumes append_rule[sep_heap_rules]: 
     "<is_list l p> append a p <is_list (l@[a])>\<^sub>t"
 
 locale imp_list_prepend = imp_list +
   constrains is_list :: "'a list \<Rightarrow> 'l \<Rightarrow> assn"
   fixes prepend :: "'a \<Rightarrow> 'l \<Rightarrow> 'l Heap"
   assumes prepend_rule[sep_heap_rules]: 
     "<is_list l p> prepend a p <is_list (a#l)>\<^sub>t"
     
 locale imp_list_head = imp_list +
   constrains is_list :: "'a list \<Rightarrow> 'l \<Rightarrow> assn"
   fixes head :: "'l \<Rightarrow> 'a Heap"
   assumes head_rule[sep_heap_rules]: 
     "l\<noteq>[] \<Longrightarrow> <is_list l p> head p <\<lambda>r. is_list l p * \<up>(r=hd l)>\<^sub>t"
 
 locale imp_list_pop = imp_list +
   constrains is_list :: "'a list \<Rightarrow> 'l \<Rightarrow> assn"
   fixes pop :: "'l \<Rightarrow> ('a\<times>'l) Heap"
   assumes pop_rule[sep_heap_rules]: 
     "l\<noteq>[] \<Longrightarrow> 
       <is_list l p> 
       pop p 
       <\<lambda>(r,p'). is_list (tl l) p' * \<up>(r=hd l)>\<^sub>t"
 
 locale imp_list_rotate = imp_list +
   constrains is_list :: "'a list \<Rightarrow> 'l \<Rightarrow> assn"
   fixes rotate :: "'l \<Rightarrow> 'l Heap"
   assumes rotate_rule[sep_heap_rules]: 
     "<is_list l p> rotate p <is_list (rotate1 l)>\<^sub>t"
 
 locale imp_list_reverse = imp_list +
   constrains is_list :: "'a list \<Rightarrow> 'l \<Rightarrow> assn"
   fixes reverse :: "'l \<Rightarrow> 'l Heap"
   assumes reverse_rule[sep_heap_rules]: 
     "<is_list l p> reverse p <is_list (rev l)>\<^sub>t"
 
 locale imp_list_iterate = imp_list +
   constrains is_list :: "'a list \<Rightarrow> 'l \<Rightarrow> assn"
   fixes is_it :: "'a list \<Rightarrow> 'l \<Rightarrow> 'a list \<Rightarrow> 'it \<Rightarrow> assn"
   fixes it_init :: "'l \<Rightarrow> ('it) Heap"
   fixes it_has_next :: "'it \<Rightarrow> bool Heap"
   fixes it_next :: "'it \<Rightarrow> ('a\<times>'it) Heap"
   assumes it_init_rule[sep_heap_rules]: 
     "<is_list l p> it_init p <is_it l p l>\<^sub>t"
   assumes it_next_rule[sep_heap_rules]: "l'\<noteq>[] \<Longrightarrow> 
     <is_it l p l' it> 
       it_next it 
-    <\<lambda>(a,it'). is_it l p (tl l') it' * \<up>(a=hd l')>"
+    <\<lambda>(a,it'). is_it l p (tl l') it' * \<up>(a=hd l')>\<^sub>t"
   assumes it_has_next_rule[sep_heap_rules]: 
     "<is_it l p l' it> 
        it_has_next it 
-     <\<lambda>r. is_it l p l' it * \<up>(r\<longleftrightarrow>l'\<noteq>[])>"
+     <\<lambda>r. is_it l p l' it * \<up>(r\<longleftrightarrow>l'\<noteq>[])>\<^sub>t"
   assumes quit_iteration:
     "is_it l p l' it \<Longrightarrow>\<^sub>A is_list l p * true"
 
 end
diff --git a/thys/Separation_Logic_Imperative_HOL/Examples/Imp_Map_Spec.thy b/thys/Separation_Logic_Imperative_HOL/Examples/Imp_Map_Spec.thy
--- a/thys/Separation_Logic_Imperative_HOL/Examples/Imp_Map_Spec.thy
+++ b/thys/Separation_Logic_Imperative_HOL/Examples/Imp_Map_Spec.thy
@@ -1,92 +1,92 @@
 section \<open>Interface for Maps\<close>
 theory Imp_Map_Spec
 imports "../Sep_Main"
 begin
 text \<open>
   This file specifies an abstract interface for map data structures. It can
   be implemented by concrete map data structures, as demonstrated in the 
   hash map example.
 \<close>
 
 locale imp_map = 
   fixes is_map :: "('k \<rightharpoonup> 'v) \<Rightarrow> 'm \<Rightarrow> assn"
   assumes precise: "precise is_map"
 
 locale imp_map_empty = imp_map +
   constrains is_map :: "('k \<rightharpoonup> 'v) \<Rightarrow> 'm \<Rightarrow> assn"
   fixes empty :: "'m Heap"
   assumes empty_rule[sep_heap_rules]: "<emp> empty <is_map Map.empty>\<^sub>t"
 
 locale imp_map_is_empty = imp_map +
   constrains is_map :: "('k \<rightharpoonup> 'v) \<Rightarrow> 'm \<Rightarrow> assn"
   fixes is_empty :: "'m \<Rightarrow> bool Heap"
   assumes is_empty_rule[sep_heap_rules]: 
     "<is_map m p> is_empty p <\<lambda>r. is_map m p * \<up>(r \<longleftrightarrow> m=Map.empty)>\<^sub>t"
 
 locale imp_map_lookup = imp_map +
   constrains is_map :: "('k \<rightharpoonup> 'v) \<Rightarrow> 'm \<Rightarrow> assn"
   fixes lookup :: "'k \<Rightarrow> 'm \<Rightarrow> ('v option) Heap"
   assumes lookup_rule[sep_heap_rules]: 
     "<is_map m p> lookup k p <\<lambda>r. is_map m p * \<up>(r = m k)>\<^sub>t"
 
 locale imp_map_update = imp_map +
   constrains is_map :: "('k \<rightharpoonup> 'v) \<Rightarrow> 'm \<Rightarrow> assn"
   fixes update :: "'k \<Rightarrow> 'v \<Rightarrow> 'm \<Rightarrow> 'm Heap"
   assumes update_rule[sep_heap_rules]: 
     "<is_map m p> update k v p <is_map (m(k \<mapsto> v))>\<^sub>t"
     
 locale imp_map_delete = imp_map +
   constrains is_map :: "('k \<rightharpoonup> 'v) \<Rightarrow> 'm \<Rightarrow> assn"
   fixes delete :: "'k \<Rightarrow> 'm \<Rightarrow> 'm Heap"
   assumes delete_rule[sep_heap_rules]: 
     "<is_map m p> delete k p <is_map (m |` (-{k}))>\<^sub>t"
 
 locale imp_map_add = imp_map +
   constrains is_map :: "('k \<rightharpoonup> 'v) \<Rightarrow> 'm \<Rightarrow> assn"
   fixes add :: "'m \<Rightarrow> 'm \<Rightarrow> 'm Heap"
   assumes add_rule[sep_heap_rules]: 
     "<is_map m p * is_map m' p'> add p p' 
      <\<lambda>r. is_map m p * is_map m' p' * is_map (m ++ m') r>\<^sub>t"
 
 
 locale imp_map_size = imp_map +
   constrains is_map :: "('k \<rightharpoonup> 'v) \<Rightarrow> 'm \<Rightarrow> assn"
   fixes size :: "'m \<Rightarrow> nat Heap"
   assumes size_rule[sep_heap_rules]: 
     "<is_map m p> size p <\<lambda>r. is_map m p * \<up>(r = card (dom m))>\<^sub>t"
 
 locale imp_map_iterate = imp_map +
   constrains is_map :: "('k \<rightharpoonup> 'v) \<Rightarrow> 'm \<Rightarrow> assn"
   fixes is_it :: "('k \<rightharpoonup> 'v) \<Rightarrow> 'm \<Rightarrow> ('k \<rightharpoonup> 'v) \<Rightarrow> 'it \<Rightarrow> assn"
   fixes it_init :: "'m \<Rightarrow> ('it) Heap"
   fixes it_has_next :: "'it \<Rightarrow> bool Heap"
   fixes it_next :: "'it \<Rightarrow> (('k\<times>'v)\<times>'it) Heap"
   assumes it_init_rule[sep_heap_rules]: 
     "<is_map s p> it_init p <is_it s p s>\<^sub>t"
   assumes it_next_rule[sep_heap_rules]: "m'\<noteq>Map.empty \<Longrightarrow> 
     <is_it m p m' it> 
       it_next it 
-    <\<lambda>((k,v),it'). is_it m p (m' |` (-{k})) it' * \<up>(m' k = Some v)>"
+    <\<lambda>((k,v),it'). is_it m p (m' |` (-{k})) it' * \<up>(m' k = Some v)>\<^sub>t"
   assumes it_has_next_rule[sep_heap_rules]: 
-    "<is_it m p m' it> it_has_next it <\<lambda>r. is_it m p m' it * \<up>(r\<longleftrightarrow>m'\<noteq>Map.empty)>"
+    "<is_it m p m' it> it_has_next it <\<lambda>r. is_it m p m' it * \<up>(r\<longleftrightarrow>m'\<noteq>Map.empty)>\<^sub>t"
   assumes quit_iteration:
     "is_it m p m' it \<Longrightarrow>\<^sub>A is_map m p * true"
 
 locale imp_map_iterate' = imp_map +
   constrains is_map :: "('k \<rightharpoonup> 'v) \<Rightarrow> 'm \<Rightarrow> assn"
   fixes is_it :: "('k \<rightharpoonup> 'v) \<Rightarrow> 'm \<Rightarrow> ('k\<times>'v) list \<Rightarrow> 'it \<Rightarrow> assn"
   fixes it_init :: "'m \<Rightarrow> ('it) Heap"
   fixes it_has_next :: "'it \<Rightarrow> bool Heap"
   fixes it_next :: "'it \<Rightarrow> (('k\<times>'v)\<times>'it) Heap"
   assumes it_init_rule[sep_heap_rules]: 
     "<is_map s p> it_init p <\<lambda>r. \<exists>\<^sub>Al. \<up>(map_of l = s) * is_it s p l r>\<^sub>t"
   assumes it_next_rule[sep_heap_rules]: " 
     <is_it m p (kv#l) it> 
       it_next it 
     <\<lambda>(kv',it'). is_it m p l it' * \<up>(kv'=kv)>"
   assumes it_has_next_rule[sep_heap_rules]: 
     "<is_it m p l it> it_has_next it <\<lambda>r. is_it m p l it * \<up>(r\<longleftrightarrow>l\<noteq>[])>"
   assumes quit_iteration:
     "is_it m p l it \<Longrightarrow>\<^sub>A is_map m p * true"
 
 end
diff --git a/thys/Separation_Logic_Imperative_HOL/Examples/Imp_Set_Spec.thy b/thys/Separation_Logic_Imperative_HOL/Examples/Imp_Set_Spec.thy
--- a/thys/Separation_Logic_Imperative_HOL/Examples/Imp_Set_Spec.thy
+++ b/thys/Separation_Logic_Imperative_HOL/Examples/Imp_Set_Spec.thy
@@ -1,67 +1,67 @@
 section \<open>Interface for Sets\<close>
 theory Imp_Set_Spec
 imports "../Sep_Main"
 begin
 text \<open>
   This file specifies an abstract interface for set data structures. It can
   be implemented by concrete set data structures, as demonstrated in the 
   hash set example.
 \<close>
 
 locale imp_set =
   fixes is_set :: "'a set \<Rightarrow> 's \<Rightarrow> assn"
   assumes precise: "precise is_set"
 
 locale imp_set_empty = imp_set +
   constrains is_set :: "'a set \<Rightarrow> 's \<Rightarrow> assn"
   fixes empty :: "'s Heap"
   assumes empty_rule[sep_heap_rules]: "<emp> empty <is_set {}>\<^sub>t"
 
 locale imp_set_is_empty = imp_set +
   constrains is_set :: "'a set \<Rightarrow> 's \<Rightarrow> assn"
   fixes is_empty :: "'s \<Rightarrow> bool Heap"
   assumes is_empty_rule[sep_heap_rules]: 
     "<is_set s p> is_empty p <\<lambda>r. is_set s p * \<up>(r \<longleftrightarrow> s={})>\<^sub>t"
 
 locale imp_set_memb = imp_set +
   constrains is_set :: "'a set \<Rightarrow> 's \<Rightarrow> assn"
   fixes memb :: "'a \<Rightarrow> 's \<Rightarrow> bool Heap"
   assumes memb_rule[sep_heap_rules]: 
     "<is_set s p> memb a p <\<lambda>r. is_set s p * \<up>(r \<longleftrightarrow> a \<in> s)>\<^sub>t"
 
 locale imp_set_ins = imp_set +
   constrains is_set :: "'a set \<Rightarrow> 's \<Rightarrow> assn"
   fixes ins :: "'a \<Rightarrow> 's \<Rightarrow> 's Heap"
   assumes ins_rule[sep_heap_rules]: 
     "<is_set s p> ins a p <is_set (Set.insert a s)>\<^sub>t"
     
 locale imp_set_delete = imp_set +
   constrains is_set :: "'a set \<Rightarrow> 's \<Rightarrow> assn"
   fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's Heap"
   assumes delete_rule[sep_heap_rules]: 
     "<is_set s p> delete a p <is_set (s - {a})>\<^sub>t"
 
 locale imp_set_size = imp_set +
   constrains is_set :: "'a set \<Rightarrow> 's \<Rightarrow> assn"
   fixes size :: "'s \<Rightarrow> nat Heap"
   assumes size_rule[sep_heap_rules]: 
     "<is_set s p> size p <\<lambda>r. is_set s p * \<up>(r = card s)>\<^sub>t"
 
 locale imp_set_iterate = imp_set +
   constrains is_set :: "'a set \<Rightarrow> 's \<Rightarrow> assn"
   fixes is_it :: "'a set \<Rightarrow> 's \<Rightarrow> 'a set \<Rightarrow> 'it \<Rightarrow> assn"
   fixes it_init :: "'s \<Rightarrow> ('it) Heap"
   fixes it_has_next :: "'it \<Rightarrow> bool Heap"
   fixes it_next :: "'it \<Rightarrow> ('a\<times>'it) Heap"
   assumes it_init_rule[sep_heap_rules]: 
     "<is_set s p> it_init p <is_it s p s>\<^sub>t"
   assumes it_next_rule[sep_heap_rules]: "s'\<noteq>{} \<Longrightarrow> 
     <is_it s p s' it> 
       it_next it 
-    <\<lambda>(a,it'). is_it s p (s' - {a}) it' * \<up>(a \<in> s')>"
+    <\<lambda>(a,it'). is_it s p (s' - {a}) it' * \<up>(a \<in> s')>\<^sub>t"
   assumes it_has_next_rule[sep_heap_rules]: 
-    "<is_it s p s' it> it_has_next it <\<lambda>r. is_it s p s' it * \<up>(r\<longleftrightarrow>s'\<noteq>{})>"
+    "<is_it s p s' it> it_has_next it <\<lambda>r. is_it s p s' it * \<up>(r\<longleftrightarrow>s'\<noteq>{})>\<^sub>t"
   assumes quit_iteration:
     "is_it s p s' it \<Longrightarrow>\<^sub>A is_set s p * true"
 
 end
diff --git a/thys/Separation_Logic_Imperative_HOL/Examples/Open_List.thy b/thys/Separation_Logic_Imperative_HOL/Examples/Open_List.thy
--- a/thys/Separation_Logic_Imperative_HOL/Examples/Open_List.thy
+++ b/thys/Separation_Logic_Imperative_HOL/Examples/Open_List.thy
@@ -1,302 +1,303 @@
 section \<open>Open Singly Linked Lists\<close>
 theory Open_List
 imports List_Seg Imp_List_Spec
 begin
 
 subsection \<open>Definitions\<close>
 type_synonym 'a os_list = "'a node ref option"
 
 abbreviation os_list :: "'a list \<Rightarrow> ('a::heap) os_list \<Rightarrow> assn" where
   "os_list l p \<equiv> lseg l p None"
 
 subsection \<open>Precision\<close>
 lemma os_prec: 
   "precise os_list"
   by rule (simp add: lseg_prec2)
 
 lemma os_imp_list_impl: "imp_list os_list"
   apply unfold_locales
   apply (rule os_prec)
   done
 interpretation os: imp_list os_list by (rule os_imp_list_impl)
 
 subsection \<open>Operations\<close>
 subsubsection \<open>Allocate Empty List\<close>
 
 definition os_empty :: "'a::heap os_list Heap" where
   "os_empty \<equiv> return None"
 
 lemma os_empty_rule: "<emp> os_empty <os_list []>"
   unfolding os_empty_def
   apply sep_auto
   done
 
 lemma os_empty_impl: "imp_list_empty os_list os_empty"
   apply unfold_locales
   apply (sep_auto heap add: os_empty_rule)
   done
 interpretation os: imp_list_empty os_list os_empty by (rule os_empty_impl)
   
 subsubsection \<open>Emptiness check\<close>
 text \<open>A linked list is empty, iff it is the null pointer.\<close>
 
 definition os_is_empty :: "'a::heap os_list \<Rightarrow> bool Heap" where
   "os_is_empty b \<equiv> return (b = None)"
 
 lemma os_is_empty_rule: 
   "<os_list xs b> os_is_empty b <\<lambda>r. os_list xs b * \<up>(r \<longleftrightarrow> xs = [])>"
   unfolding os_is_empty_def
   apply sep_auto
   done
 
 lemma os_is_empty_impl: "imp_list_is_empty os_list os_is_empty"
   apply unfold_locales
   apply (sep_auto heap add: os_is_empty_rule)
   done
 interpretation os: imp_list_is_empty os_list os_is_empty
   by (rule os_is_empty_impl)
 
 subsubsection \<open>Prepend\<close>
 
 text \<open>To push an element to the front of a list we allocate a new node which
   stores the element and the old list as successor. The new list is the new 
   allocated reference.\<close>
 
 definition os_prepend :: "'a \<Rightarrow> 'a::heap os_list \<Rightarrow> 'a os_list Heap" where
   "os_prepend a n = do { p \<leftarrow> ref (Node a n); return (Some p) }"
 
 lemma os_prepend_rule:
   "<os_list xs n> os_prepend x n <os_list (x # xs)>"
   unfolding os_prepend_def
   apply sep_auto
   done
 
 lemma os_prepend_impl: "imp_list_prepend os_list os_prepend"
   apply unfold_locales
   apply (sep_auto heap add: os_prepend_rule)
   done
 interpretation os: imp_list_prepend os_list os_prepend 
   by (rule os_prepend_impl)
 
 subsubsection\<open>Pop\<close>
 text \<open>To pop the first element out of the list we look up the value and the
   reference of the node and return the pair of those.\<close>
 
 fun os_pop :: "'a::heap os_list \<Rightarrow> ('a \<times> 'a os_list) Heap" where
   "os_pop None   = raise STR ''Empty Os_list''" |
   "os_pop (Some p) = do {m \<leftarrow> !p; return (val m, next m)}"
 
 declare os_pop.simps[simp del]
 
 lemma os_pop_rule:
   "xs \<noteq> [] \<Longrightarrow> <os_list xs r> 
   os_pop r 
   <\<lambda>(x,r'). os_list (tl xs) r' * (the r) \<mapsto>\<^sub>r (Node x r') * \<up>(x = hd xs)>"
 
   apply (cases r, simp_all)
   apply (cases xs, simp_all)
 
   apply (sep_auto simp: os_pop.simps)
   done
 
 lemma os_pop_impl: "imp_list_pop os_list os_pop"
   apply unfold_locales
   apply (sep_auto heap add: os_pop_rule)
   done
 interpretation os: imp_list_pop os_list os_pop by (rule os_pop_impl)
 
 subsubsection \<open>Reverse\<close>
 
 text \<open>The following reversal function is equivalent to the one from 
   Imperative HOL. And gives a more difficult example.\<close>
 
 partial_function (heap) os_reverse_aux 
   :: "'a::heap os_list \<Rightarrow> 'a os_list \<Rightarrow> 'a os_list Heap" 
   where [code]:
   "os_reverse_aux q p = (case p of 
     None \<Rightarrow> return q |
     Some r \<Rightarrow> do {
       v \<leftarrow> !r;
       r := Node (val v) q;
       os_reverse_aux p (next v) })"
 
 lemma [simp, sep_dflt_simps]:
   "os_reverse_aux q None = return q"
   "os_reverse_aux q (Some r) = do {
       v \<leftarrow> !r;
       r := Node (val v) q;
       os_reverse_aux (Some r) (next v) }"
   apply (subst os_reverse_aux.simps)
   apply simp
   apply (subst os_reverse_aux.simps)
   apply simp
   done
 
 definition "os_reverse p = os_reverse_aux None p"
 
 lemma os_reverse_aux_rule: 
   "<os_list xs p * os_list ys q> 
     os_reverse_aux q p 
   <os_list ((rev xs) @ ys) >"
 proof (induct xs arbitrary: p q ys)
   case Nil thus ?case
     apply sep_auto
     done
 next
   case (Cons x xs)
   show ?case
     apply (cases p, simp_all)
     apply (sep_auto heap add: cons_pre_rule[OF _ Cons.hyps])
     done
 qed
 
 lemma os_reverse_rule: "<os_list xs p> os_reverse p <os_list (rev xs)>"
   unfolding os_reverse_def
   apply (auto simp: os_reverse_aux_rule[where ys="[]", simplified, rule_format])
   done
 
 lemma os_reverse_impl: "imp_list_reverse os_list os_reverse"
   apply unfold_locales
   apply (sep_auto heap add: os_reverse_rule)
   done
 interpretation os: imp_list_reverse os_list os_reverse
   by (rule os_reverse_impl)
 
 subsubsection \<open>Remove\<close>
  
 text \<open>Remove all appearances of an element from a linked list.\<close>
 
 partial_function (heap) os_rem 
   :: "'a::heap \<Rightarrow> 'a node ref option \<Rightarrow> 'a node ref option Heap" 
   where [code]:
   "os_rem x b = (case b of 
      None \<Rightarrow> return None |
      Some p \<Rightarrow> do { 
        n \<leftarrow> !p;
        q \<leftarrow> os_rem x (next n);
        (if (val n = x) 
          then return q
          else do { 
            p := Node (val n) q; 
            return (Some p) }) })"
 
 lemma [simp, sep_dflt_simps]: 
   "os_rem x None = return None"
   "os_rem x (Some p) = do { 
        n \<leftarrow> !p;
        q \<leftarrow> os_rem x (next n);
        (if (val n = x) 
          then return q
          else do { 
            p := Node (val n) q; 
            return (Some p) }) }"
   apply (subst os_rem.simps, simp)+
   done
 
 lemma os_rem_rule[sep_heap_rules]: 
   "<os_list xs b> os_rem x b <\<lambda>r. os_list (removeAll x xs) r * true>"
 proof (induct xs arbitrary: b x) (* Have to generalize over x, as 
     sep_auto preprocessor introduces a new variable. Alternative: 
     No preprocessing. (See alternative proof below) *)
   case Nil show ?case
     apply sep_auto
     done
 next
   case (Cons y xs) 
   show ?case by (sep_auto heap add: Cons.hyps)
 qed
 
 lemma os_rem_rule_alt_proof: 
   "<os_list xs b> os_rem x b <\<lambda>r. os_list (removeAll x xs) r * true>"
 proof (induct xs arbitrary: b) 
   case Nil show ?case
     apply sep_auto
     done
 next
   case (Cons y xs)
   show ?case 
     by (sep_auto (nopre) heap add: Cons.hyps) (* Switching off preprocessor *)
 qed
 
 subsubsection \<open>Iterator\<close>
 
 type_synonym 'a os_list_it = "'a os_list"
 definition "os_is_it l p l2 it 
   \<equiv> \<exists>\<^sub>Al1. \<up>(l=l1@l2) * lseg l1 p it * os_list l2 it"
 
 definition os_it_init :: "'a os_list \<Rightarrow> ('a os_list_it) Heap" 
   where "os_it_init l = return l"
 
 fun os_it_next where 
   "os_it_next (Some p) = do {
     n \<leftarrow> !p;
     return (val n,next n)
   }"
 
 definition os_it_has_next :: "'a os_list_it \<Rightarrow> bool Heap" where
   "os_it_has_next it \<equiv> return (it\<noteq>None)"
 
 lemma os_iterate_impl: 
   "imp_list_iterate os_list os_is_it os_it_init os_it_has_next os_it_next"
   apply unfold_locales
   unfolding os_it_init_def os_is_it_def[abs_def] 
   apply sep_auto
 
   apply (case_tac it, simp)
   apply (case_tac l', simp)
   apply sep_auto
   apply (rule ent_frame_fwd[OF lseg_append])
     apply frame_inference
     apply simp
+  apply (sep_auto)
 
   unfolding os_it_has_next_def
   apply (sep_auto elim!: neq_NilE)
 
   apply solve_entails
   apply (rule ent_frame_fwd[OF lseg_conc])
     apply frame_inference
     apply solve_entails
   done
 interpretation os: 
   imp_list_iterate os_list os_is_it os_it_init os_it_has_next os_it_next
   by (rule os_iterate_impl)
 
 subsubsection \<open>List-Sum\<close>
 
 partial_function (heap) os_sum' :: "int os_list_it \<Rightarrow> int \<Rightarrow> int Heap" 
   where [code]:
   "os_sum' it s = do {
     b \<leftarrow> os_it_has_next it;
     if b then do {
       (x,it') \<leftarrow> os_it_next it;
       os_sum' it' (s+x)
     } else return s
   }"
 
 lemma os_sum'_rule[sep_heap_rules]: 
   "<os_is_it l p l' it> 
     os_sum' it s 
   <\<lambda>r. os_list l p * \<up>(r = s + sum_list l')>\<^sub>t"
 proof (induct l' arbitrary: it s)
   case Nil thus ?case
     apply (subst os_sum'.simps)
-    apply (sep_auto intro: os.quit_iteration)
+    apply (sep_auto intro: os.quit_iteration ent_true_drop(1))
     done
 next
   case (Cons x l')
   show ?case
     apply (subst os_sum'.simps)
     apply (sep_auto heap: Cons.hyps)
     done
 qed
 
 definition "os_sum p \<equiv> do { 
   it \<leftarrow> os_it_init p;
   os_sum' it 0}"
 
 lemma os_sum_rule[sep_heap_rules]: 
   "<os_list l p> os_sum p <\<lambda>r. os_list l p * \<up>(r=sum_list l)>\<^sub>t"
   unfolding os_sum_def
   by sep_auto
 
 end