--- a/src/HOL/Hoare/List_Examples.ML Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/Hoare/List_Examples.ML Thu Sep 26 12:47:47 1996 +0200
@@ -6,11 +6,11 @@
\ y := hd x # y; x := tl x \
\ END \
\{y=rev(X)}";
-by(hoare_tac 1);
-by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
-by(safe_tac (!claset));
-by(Asm_full_simp_tac 1);
-by(Asm_full_simp_tac 1);
+by (hoare_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
+by (safe_tac (!claset));
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
qed "imperative_reverse";
goal thy
@@ -21,9 +21,9 @@
\ y := hd x # y; x := tl x \
\ END \
\{y = X@Y}";
-by(hoare_tac 1);
-by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
-by(safe_tac (!claset));
-by(Asm_full_simp_tac 1);
-by(Asm_full_simp_tac 1);
+by (hoare_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
+by (safe_tac (!claset));
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
qed "imperative_append";