src/HOL/Set.ML
changeset 4477 b3e5857d8d99
parent 4469 399868bf8444
child 4510 a37f515a0b25
     1.1 --- a/src/HOL/Set.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/Set.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -470,7 +470,7 @@
     1.4  
     1.5  (*The order of the premises presupposes that A is rigid; b may be flexible*)
     1.6  goal Set.thy "!!b. [| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))";
     1.7 -by (Auto_tac());
     1.8 +by Auto_tac;
     1.9  qed "UN_I";
    1.10  
    1.11  val major::prems = goalw Set.thy [UNION_def]
    1.12 @@ -494,7 +494,7 @@
    1.13  section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";
    1.14  
    1.15  goalw Set.thy [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))";
    1.16 -by (Auto_tac());
    1.17 +by Auto_tac;
    1.18  qed "INT_iff";
    1.19  
    1.20  Addsimps [INT_iff];
    1.21 @@ -505,7 +505,7 @@
    1.22  qed "INT_I";
    1.23  
    1.24  goal Set.thy "!!b. [| b : (INT x:A. B(x));  a:A |] ==> b: B(a)";
    1.25 -by (Auto_tac());
    1.26 +by Auto_tac;
    1.27  qed "INT_D";
    1.28  
    1.29  (*"Classical" elimination -- by the Excluded Middle on a:A *)
    1.30 @@ -537,7 +537,7 @@
    1.31  
    1.32  (*The order of the premises presupposes that C is rigid; A may be flexible*)
    1.33  goal Set.thy "!!X. [| X:C;  A:X |] ==> A : Union(C)";
    1.34 -by (Auto_tac());
    1.35 +by Auto_tac;
    1.36  qed "UnionI";
    1.37  
    1.38  val major::prems = goalw Set.thy [Union_def]
    1.39 @@ -566,7 +566,7 @@
    1.40  (*A "destruct" rule -- every X in C contains A as an element, but
    1.41    A:X can hold when X:C does not!  This rule is analogous to "spec". *)
    1.42  goal Set.thy "!!X. [| A : Inter(C);  X:C |] ==> A:X";
    1.43 -by (Auto_tac());
    1.44 +by Auto_tac;
    1.45  qed "InterD";
    1.46  
    1.47  (*"Classical" elimination rule -- does not require proving X:C *)
    1.48 @@ -672,7 +672,7 @@
    1.49  
    1.50  goalw Set.thy [psubset_def]
    1.51      "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
    1.52 -by (Auto_tac());
    1.53 +by Auto_tac;
    1.54  qed "psubset_insertD";
    1.55  
    1.56  bind_thm ("psubset_eq", psubset_def RS meta_eq_to_obj_eq);