src/HOL/Data_Structures/Tree23_Set.thy
changeset 61588 1d2907d0ed73
parent 61581 00d9682e8dd7
child 61640 44c9198f210c
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Thu Nov 05 11:59:45 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Thu Nov 05 18:38:08 2015 +0100
@@ -356,7 +356,7 @@
 
 interpretation Set_by_Ordered
 where empty = Leaf and isin = isin and insert = insert and delete = delete
-and inorder = inorder and wf = bal
+and inorder = inorder and inv = bal
 proof (standard, goal_cases)
   case 2 thus ?case by(simp add: isin_set)
 next