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