renamed variables for clarity
authorpaulson
Wed Jan 20 10:33:34 1999 +0100 (1999-01-20)
changeset 614600f3324048a7
parent 6145 dea357e84ac9
child 6147 345c0fb3e628
renamed variables for clarity
src/HOL/ex/set.ML
     1.1 --- a/src/HOL/ex/set.ML	Wed Jan 20 10:29:25 1999 +0100
     1.2 +++ b/src/HOL/ex/set.ML	Wed Jan 20 10:33:34 1999 +0100
     1.3 @@ -19,12 +19,12 @@
     1.4  (** Examples for the Blast_tac paper **)
     1.5  
     1.6  (*Union-image, called Un_Union_image on equalities.ML*)
     1.7 -Goal "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
     1.8 +Goal "(UN x:C. f(x) Un g(x)) = Union(f``C)  Un  Union(g``C)";
     1.9  by (Blast_tac 1);
    1.10  result();
    1.11  
    1.12  (*Inter-image, called Int_Inter_image on equalities.ML*)
    1.13 -Goal "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
    1.14 +Goal "(INT x:C. f(x) Int g(x)) = Inter(f``C) Int Inter(g``C)";
    1.15  by (Blast_tac 1);
    1.16  result();
    1.17