src/HOL/equalities.ML
changeset 1553 4eb4a9c7d736
parent 1548 afe750876848
child 1564 822575c737bd
     1.1 --- a/src/HOL/equalities.ML	Wed Mar 06 12:52:11 1996 +0100
     1.2 +++ b/src/HOL/equalities.ML	Wed Mar 06 13:57:07 1996 +0100
     1.3 @@ -13,24 +13,24 @@
     1.4  section "{}";
     1.5  
     1.6  goal Set.thy "{x.False} = {}";
     1.7 -by(fast_tac eq_cs 1);
     1.8 +by (fast_tac eq_cs 1);
     1.9  qed "Collect_False_empty";
    1.10  Addsimps [Collect_False_empty];
    1.11  
    1.12  goal Set.thy "(A <= {}) = (A = {})";
    1.13 -by(fast_tac eq_cs 1);
    1.14 +by (fast_tac eq_cs 1);
    1.15  qed "subset_empty";
    1.16  Addsimps [subset_empty];
    1.17  
    1.18  section ":";
    1.19  
    1.20  goal Set.thy "x ~: {}";
    1.21 -by(fast_tac set_cs 1);
    1.22 +by (fast_tac set_cs 1);
    1.23  qed "in_empty";
    1.24  Addsimps[in_empty];
    1.25  
    1.26  goal Set.thy "x : insert y A = (x=y | x:A)";
    1.27 -by(fast_tac set_cs 1);
    1.28 +by (fast_tac set_cs 1);
    1.29  qed "in_insert";
    1.30  Addsimps[in_insert];
    1.31  
    1.32 @@ -38,7 +38,7 @@
    1.33  
    1.34  (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
    1.35  goal Set.thy "insert a A = {a} Un A";
    1.36 -by(fast_tac eq_cs 1);
    1.37 +by (fast_tac eq_cs 1);
    1.38  qed "insert_is_Un";
    1.39  
    1.40  goal Set.thy "insert a A ~= {}";
    1.41 @@ -54,7 +54,7 @@
    1.42  qed "insert_absorb";
    1.43  
    1.44  goal Set.thy "insert x (insert x A) = insert x A";
    1.45 -by(fast_tac eq_cs 1);
    1.46 +by (fast_tac eq_cs 1);
    1.47  qed "insert_absorb2";
    1.48  Addsimps [insert_absorb2];
    1.49  
    1.50 @@ -65,8 +65,8 @@
    1.51  
    1.52  (* use new B rather than (A-{a}) to avoid infinite unfolding *)
    1.53  goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
    1.54 -by(res_inst_tac [("x","A-{a}")] exI 1);
    1.55 -by(fast_tac eq_cs 1);
    1.56 +by (res_inst_tac [("x","A-{a}")] exI 1);
    1.57 +by (fast_tac eq_cs 1);
    1.58  qed "mk_disjoint_insert";
    1.59  
    1.60  section "''";
    1.61 @@ -145,27 +145,27 @@
    1.62  qed "Un_assoc";
    1.63  
    1.64  goal Set.thy "{} Un B = B";
    1.65 -by(fast_tac eq_cs 1);
    1.66 +by (fast_tac eq_cs 1);
    1.67  qed "Un_empty_left";
    1.68  Addsimps[Un_empty_left];
    1.69  
    1.70  goal Set.thy "A Un {} = A";
    1.71 -by(fast_tac eq_cs 1);
    1.72 +by (fast_tac eq_cs 1);
    1.73  qed "Un_empty_right";
    1.74  Addsimps[Un_empty_right];
    1.75  
    1.76  goal Set.thy "UNIV Un B = UNIV";
    1.77 -by(fast_tac eq_cs 1);
    1.78 +by (fast_tac eq_cs 1);
    1.79  qed "Un_UNIV_left";
    1.80  Addsimps[Un_UNIV_left];
    1.81  
    1.82  goal Set.thy "A Un UNIV = UNIV";
    1.83 -by(fast_tac eq_cs 1);
    1.84 +by (fast_tac eq_cs 1);
    1.85  qed "Un_UNIV_right";
    1.86  Addsimps[Un_UNIV_right];
    1.87  
    1.88  goal Set.thy "insert a B Un C = insert a (B Un C)";
    1.89 -by(fast_tac eq_cs 1);
    1.90 +by (fast_tac eq_cs 1);
    1.91  qed "Un_insert_left";
    1.92  
    1.93  goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
    1.94 @@ -437,7 +437,7 @@
    1.95  Addsimps[Diff_UNIV];
    1.96  
    1.97  goal Set.thy "!!x. x~:A ==> A - insert x B = A-B";
    1.98 -by(fast_tac eq_cs 1);
    1.99 +by (fast_tac eq_cs 1);
   1.100  qed "Diff_insert0";
   1.101  Addsimps [Diff_insert0];
   1.102  
   1.103 @@ -452,12 +452,12 @@
   1.104  qed "Diff_insert2";
   1.105  
   1.106  goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
   1.107 -by(simp_tac (!simpset setloop split_tac[expand_if]) 1);
   1.108 -by(fast_tac eq_cs 1);
   1.109 +by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
   1.110 +by (fast_tac eq_cs 1);
   1.111  qed "insert_Diff_if";
   1.112  
   1.113  goal Set.thy "!!x. x:B ==> insert x A - B = A-B";
   1.114 -by(fast_tac eq_cs 1);
   1.115 +by (fast_tac eq_cs 1);
   1.116  qed "insert_Diff1";
   1.117  Addsimps [insert_Diff1];
   1.118