blob: 28d0bd556d81d4d617236d758e556aa54da50854 (
plain)
1
2
3
4
5
6
7
|
(* Test pattern with dependent occurrences; Note that it does not
behave as the succession of three generalize because each
quantification introduces new occurrences that are automatically
abstracted with the numbering still based on the original statement *)
Goal (id true,id false)=(id true,id true).
generalize bool at 2 4 6 8 10 as B, true at 3 as tt, false as ff.
|
