src/HOL/Induct/LFilter.ML
changeset 4477 b3e5857d8d99
parent 4090 9f1eaab75e8c
child 4521 c7f56322a84b
     1.1 --- a/src/HOL/Induct/LFilter.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/Induct/LFilter.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -190,7 +190,7 @@
     1.4  (*Cases: p x is true or false*)
     1.5  by (rtac (lfilter_cases RS disjE) 1);
     1.6  by (etac ssubst 1);
     1.7 -by (Auto_tac());
     1.8 +by Auto_tac;
     1.9  qed "lfilter_idem";
    1.10  
    1.11  
    1.12 @@ -211,7 +211,7 @@
    1.13  \              ==> (l, LCons x l') : findRel q --> ~ p x     \
    1.14  \                  --> l' : Domain (findRel (%x. p x & q x))";
    1.15  by (etac findRel.induct 1);
    1.16 -by (Auto_tac());
    1.17 +by Auto_tac;
    1.18  qed_spec_mp "findRel_not_conj_Domain";
    1.19  
    1.20  
    1.21 @@ -229,9 +229,9 @@
    1.22  by (etac findRel.induct 1);
    1.23  by (blast_tac (claset() addSDs [sym RS lfilter_eq_LCons]
    1.24                         addIs  [findRel_conj]) 1);
    1.25 -by (Auto_tac());
    1.26 +by Auto_tac;
    1.27  by (dtac (sym RS lfilter_eq_LCons) 1);
    1.28 -by (Auto_tac());
    1.29 +by Auto_tac;
    1.30  by (dtac spec 1);
    1.31  by (dtac (refl RS rev_mp) 1);
    1.32  by (blast_tac (claset() addIs [findRel_conj2]) 1);
    1.33 @@ -303,7 +303,7 @@
    1.34  \              (EX y l''. x = f y & l' = lmap f l'' & l = LCons y l'')";
    1.35  by (stac (lmap_def RS def_llist_corec) 1);
    1.36  by (res_inst_tac [("l", "l")] llistE 1);
    1.37 -by (Auto_tac());
    1.38 +by Auto_tac;
    1.39  qed_spec_mp "lmap_eq_LCons";
    1.40  
    1.41