src/HOL/Option.ML
changeset 2031 03a843f0f447
parent 2019 b45d9f2042e0
child 2056 93c093620c28
--- a/src/HOL/Option.ML	Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/Option.ML	Thu Sep 26 12:47:47 1996 +0200
@@ -27,5 +27,5 @@
 by (option.induct_tac "opt" 1);
 by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
-by(Fast_tac 1);
+by (Fast_tac 1);
 qed"expand_option_case";