src/HOL/IMP/Natural.ML

--- a/src/HOL/IMP/Natural.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/IMP/Natural.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -31,20 +31,20 @@
 
 Goal "[| !x. P x --> Q x; <w,s> -c-> t |] ==> \
 \ !c. w = While P c --> <While Q c,t> -c-> u --> <While Q c,s> -c-> u";
-be evalc.induct 1;
-by(Auto_tac);
+by (etac evalc.induct 1);
+by (Auto_tac);
 val lemma1 = result() RS spec RS mp RS mp;
 
 Goal "[| !x. P x --> Q x; <w,s> -c-> u |] ==> \
 \ !c. w = While Q c --> <While P c; While Q c,s> -c-> u";
-be evalc.induct 1;
-by(ALLGOALS Asm_simp_tac);
-by(Blast_tac 1);
-by(case_tac "P s" 1);
-by(Auto_tac);
+by (etac evalc.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
+by (case_tac "P s" 1);
+by (Auto_tac);
 val lemma2 = result() RS spec RS mp;
 
 Goal "!x. P x --> Q x ==> \
 \ (<While P c; While Q c, s> -c-> t) = (<While Q c, s> -c-> t)";
-by(blast_tac (claset() addIs [lemma1,lemma2]) 1);
+by (blast_tac (claset() addIs [lemma1,lemma2]) 1);
 qed "Hoare_example";