src/HOL/Data_Structures/Tree_Map.thy
changeset 61686 e6784939d645
parent 61651 415e816d3f37
child 61790 0494964bb226
     1.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Mon Nov 16 12:37:46 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Mon Nov 16 13:08:52 2015 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4  
     1.5  interpretation Map_by_Ordered
     1.6  where empty = Leaf and lookup = lookup and update = update and delete = delete
     1.7 -and inorder = inorder and wf = "\<lambda>_. True"
     1.8 +and inorder = inorder and inv = "\<lambda>_. True"
     1.9  proof (standard, goal_cases)
    1.10    case 1 show ?case by simp
    1.11  next
    1.12 @@ -53,6 +53,6 @@
    1.13    case 3 thus ?case by(simp add: inorder_update)
    1.14  next
    1.15    case 4 thus ?case by(simp add: inorder_delete)
    1.16 -qed (rule TrueI)+
    1.17 +qed auto
    1.18  
    1.19  end