equal
deleted
inserted
replaced
17 result(); |
17 result(); |
18 |
18 |
19 (** Examples for the Blast_tac paper **) |
19 (** Examples for the Blast_tac paper **) |
20 |
20 |
21 (*Union-image, called Un_Union_image on equalities.ML*) |
21 (*Union-image, called Un_Union_image on equalities.ML*) |
22 Goal "(UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)"; |
22 Goal "(UN x:C. f(x) Un g(x)) = Union(f``C) Un Union(g``C)"; |
23 by (Blast_tac 1); |
23 by (Blast_tac 1); |
24 result(); |
24 result(); |
25 |
25 |
26 (*Inter-image, called Int_Inter_image on equalities.ML*) |
26 (*Inter-image, called Int_Inter_image on equalities.ML*) |
27 Goal "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)"; |
27 Goal "(INT x:C. f(x) Int g(x)) = Inter(f``C) Int Inter(g``C)"; |
28 by (Blast_tac 1); |
28 by (Blast_tac 1); |
29 result(); |
29 result(); |
30 |
30 |
31 (*Singleton I. Nice demonstration of blast_tac--and its limitations*) |
31 (*Singleton I. Nice demonstration of blast_tac--and its limitations*) |
32 Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"; |
32 Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"; |