src/HOL/Induct/Exp.ML
changeset 4477 b3e5857d8d99
parent 4264 5e21f41ccd21
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/Induct/Exp.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/Induct/Exp.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -109,7 +109,7 @@
     1.4  (*This theorem says that "WHILE TRUE DO c" cannot terminate*)
     1.5  goal thy "!!x. (c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
     1.6  by (etac exec.induct 1);
     1.7 -by (Auto_tac());
     1.8 +by Auto_tac;
     1.9  bind_thm ("while_true_E", refl RSN (2, result() RS mp));
    1.10  
    1.11