src/HOL/Data_Structures/Brother12_Map.thy
changeset 68431 b294e095f64c
parent 68020 6aade817bee5
     1.1 --- a/src/HOL/Data_Structures/Brother12_Map.thy	Tue Jun 12 07:18:18 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Brother12_Map.thy	Tue Jun 12 17:18:40 2018 +0200
     1.3 @@ -192,7 +192,7 @@
     1.4  subsection "Overall correctness"
     1.5  
     1.6  interpretation Map_by_Ordered
     1.7 -where empty = N0 and lookup = lookup and update = update.update
     1.8 +where empty = empty and lookup = lookup and update = update.update
     1.9  and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> B h"
    1.10  proof (standard, goal_cases)
    1.11    case 2 thus ?case by(auto intro!: lookup_map_of)
    1.12 @@ -204,6 +204,6 @@
    1.13    case 6 thus ?case using update.update_type by (metis Un_iff)
    1.14  next
    1.15    case 7 thus ?case using delete.delete_type by blast
    1.16 -qed auto
    1.17 +qed (auto simp: empty_def)
    1.18  
    1.19  end