| changeset 61428 | 5e1938107371 |
| parent 61231 | cc6969542f8d |
| child 61581 | 00d9682e8dd7 |
| 61427:3c69ea85f8dd | 61428:5e1938107371 |
|---|---|
75 case 2 thus ?case by(simp add: isin_set) |
75 case 2 thus ?case by(simp add: isin_set) |
76 next |
76 next |
77 case 3 thus ?case by(simp add: inorder_insert) |
77 case 3 thus ?case by(simp add: inorder_insert) |
78 next |
78 next |
79 case 4 thus ?case by(simp add: inorder_delete) |
79 case 4 thus ?case by(simp add: inorder_delete) |
80 next |
80 qed (rule TrueI)+ |
81 case 5 thus ?case .. |
|
82 qed |
|
83 |
81 |
84 end |
82 end |