equal
deleted
inserted
replaced
2686 apply(simp) |
2686 apply(simp) |
2687 prefer 3 |
2687 prefer 3 |
2688 apply(simp) |
2688 apply(simp) |
2689 (* AALT case *) |
2689 (* AALT case *) |
2690 prefer 2 |
2690 prefer 2 |
2691 apply(simp only:) |
2691 apply(simp only:) |
2692 (* *) |
|
2693 apply(simp) |
|
2694 apply(subst WWW5) |
|
2695 |
|
2696 |
|
2697 |
|
2698 |
|
2699 apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]") |
2692 apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]") |
2700 apply(clarify) |
2693 apply(clarify) |
2701 apply(simp del: bsimp.simps) |
2694 apply(simp del: bsimp.simps) |
2702 apply(subst (2) CT1) |
2695 apply(subst (2) CT1) |
2703 apply(simp del: bsimp.simps) |
2696 apply(simp del: bsimp.simps) |