src/HOL/Data_Structures/RBT_Set.thy
changeset 61588 1d2907d0ed73
parent 61581 00d9682e8dd7
child 61678 b594e9277be3
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Thu Nov 05 11:59:45 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Thu Nov 05 18:38:08 2015 +0100
     1.3 @@ -73,7 +73,7 @@
     1.4  
     1.5  interpretation Set_by_Ordered
     1.6  where empty = Leaf and isin = isin and insert = insert 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