summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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