src/HOL/Induct/LList.ML
changeset 4477 b3e5857d8d99
parent 4160 59826ea67cba
child 4521 c7f56322a84b
     1.1 --- a/src/HOL/Induct/LList.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/Induct/LList.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -652,7 +652,7 @@
     1.4  (*Surprisingly hard to prove.  Used with lfilter*)
     1.5  goalw thy [llistD_Fun_def, prod_fun_def]
     1.6      "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
     1.7 -by (Auto_tac());
     1.8 +by Auto_tac;
     1.9  by (rtac image_eqI 1);
    1.10  by (fast_tac (claset() addss (simpset())) 1);
    1.11  by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 1);