equal
deleted
inserted
replaced
381 apply (force simp add:Blacks_def) |
381 apply (force simp add:Blacks_def) |
382 --{* 2 subgoals left *} |
382 --{* 2 subgoals left *} |
383 apply force |
383 apply force |
384 --{* 1 subgoal left *} |
384 --{* 1 subgoal left *} |
385 apply clarify |
385 apply clarify |
386 apply(drule Nat.le_imp_less_or_eq) |
386 apply(drule_tac x = "ind x" in le_imp_less_or_eq) |
387 apply (simp_all add:Blacks_def) |
387 apply (simp_all add:Blacks_def) |
388 done |
388 done |
389 |
389 |
390 subsubsection {* Appending garbage nodes to the free list *} |
390 subsubsection {* Appending garbage nodes to the free list *} |
391 |
391 |