more precise import;
authorwenzelm
Fri Jan 14 15:43:04 2011 +0100 (2011-01-14)
changeset 415492c65ad10bec8
parent 41548 bd0bebf93fa6
child 41550 efa734d9b221
more precise import;
eliminated global prems;
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
     1.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Jan 14 13:58:07 2011 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Jan 14 15:43:04 2011 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Linked Lists by ML references *}
     1.5  
     1.6  theory Linked_Lists
     1.7 -imports Imperative_HOL Code_Integer
     1.8 +imports "../Imperative_HOL" Code_Integer
     1.9  begin
    1.10  
    1.11  section {* Definition of Linked Lists *}
    1.12 @@ -371,13 +371,12 @@
    1.13  assumes "Ref.get h1 p = Node x pn"
    1.14  assumes "refs_of' (Ref.set p (Node x r1) h1) p rs"
    1.15  obtains r1s where "rs = (p#r1s)" and "refs_of' h1 r1 r1s"
    1.16 -using assms
    1.17  proof -
    1.18    from assms refs_of'_distinct[OF assms(2)] have "\<exists> r1s. rs = (p # r1s) \<and> refs_of' h1 r1 r1s"
    1.19      apply -
    1.20      unfolding refs_of'_def'[of _ p]
    1.21      apply (auto, frule refs_of_set_ref2) by (auto dest: Ref.noteq_sym)
    1.22 -  with prems show thesis by auto
    1.23 +  with assms that show thesis by auto
    1.24  qed
    1.25  
    1.26  section {* Proving make_llist and traverse correct *}