src/HOL/ex/set.ML
 changeset 6146 00f3324048a7 parent 5786 9a2c90bdadfe child 6171 cd237a10cbf8
equal inserted replaced
6145:dea357e84ac9 6146:00f3324048a7
`    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}";`